Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Fermat's Last Theorem – how it’s going

xenaproject.wordpress.com

Post reply on HN
Print view View original

181–190 of 216 posts

Re: Fermat's Last Theorem – how it’s going

#181

Post by paulddraper »

lambdaone wrote: post #20
coliveira wrote: post #6

Earlier quoted context omitted.

> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems, a huge amount of it obviously can, as is demonstrated by the fact that we can write it down in a reasonably rigorous way in a combination of conventional mathematical notation and plain English. Nor is this in any way "a fundamental problem with using AI to do math".

> While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems

That's a misleading way of expressing that.

Math can be formalized as completely as we want, if we concede that some true statements will exist without a possible proof.

Re: Fermat's Last Theorem – how it’s going

#182

Post by mydogcanpurr »

paulddraper wrote: post #180
vouaobrasil wrote: post #24

> The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to…

Has that ever blown up their faces? I.e. a widely accepted proof that had a critical flaw due to hand waving? If it hasn't, I would understand why they'd be cavalier about explicit details.

Yes, famously the Italian school of algebraic geometry ran into foundational issues. See https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge....

Re: Fermat's Last Theorem – how it’s going

#183

Post by dang »

TechDebtDevin wrote: post #42
Etheryte wrote: post #13

Earlier quoted context omitted.

[flagged]

I don't even understand how you interpreted that to have anything to do with being "smarter or making more money". Get some more coffee dude.

Please don't respond to a bad comment by breaking the site guidelines yourself. That only makes things worse.

https://news.ycombinator.com/newsguidelines.html

Re: Fermat's Last Theorem – how it’s going

#184

Post by dang »

Etheryte wrote: post #13
bee_rider wrote: post #7

This hurts my engineer-brain. Just a reminder than the gap between us and mathematicians is about the same as the gap between us and everybody else (edit: in terms of math skills), just in the other direction, haha. Oh well, hopefully when they get the machines to solve math, they’ll still want them to run a couple percents faster every year.

[flagged]

"Please respond to the strongest plausible interpretation of what someone says, not a weaker one that's easier to criticize. Assume good faith."

https://news.ycombinator.com/newsguidelines.html

Re: Fermat's Last Theorem – how it’s going

#185

Post by gedpeck »

semolinapudding wrote: post #176
gedpeck wrote: post #164

Earlier quoted context omitted.

You know more than me on logic so I defer to your expertise. https://math.stackexchange.com/questions/4753432/g%C3%B6dels... Andreas Blass in the comments says that the Incompleteness results don’t apply to the second order Axioms (tabling about PA_2 here and not Z_2) and that the second order axioms are not computably enumerable. Maybe that’s the correct concept I was remembering from mathematical logic class. Don’t…

There's a bit of a definition issue at play here. When Andreas Blass and Noah Schweber say that there is no proof system for PA_2, they mean that there is no effective proof system that is complete for the full semantics. If you subscribe to their definition of a proof system, you end up saying that there is no such thing as a proof in PA_2, and thus that incompleteness is meaningless -- which I personally find a bit…

Thanks for the reply.

Re: Fermat's Last Theorem – how it’s going

#186

Post by gedpeck »

Tainnor wrote: post #171
gedpeck wrote: post #164

Earlier quoted context omitted.

You know more than me on logic so I defer to your expertise. https://math.stackexchange.com/questions/4753432/g%C3%B6dels... Andreas Blass in the comments says that the Incompleteness results don’t apply to the second order Axioms (tabling about PA_2 here and not Z_2) and that the second order axioms are not computably enumerable. Maybe that’s the correct concept I was remembering from mathematical logic class. Don’t…

> and that the second order axioms are not computably enumerable He says that true sentences in second order logic aren't computably enumerable, he's not talking about the axioms. > Don’t know if computably enumerable is the same as recursively enumerable I've only ever seen them used as synonyms. > Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an ax…

Thanks for the reply.

...it's decidable - otherwise, it would be impossible to decide whether a proof is valid.

Isn't that the whole issue with PA_2 vs. PA? In PA_2 with "full semantics" there is no effective procedure for determining if a statement is an axiom. In my mind this is what I mean by the incompleteness results not applying to PA_2. They do apply to Z_2 since that is an effective (computable?) system.

But Z2 is usually studied with first-order semantics, and in that context it is an effective theory of arithmetic subject to the incompleteness theorems. In particular, Z2 includes every axiom of PA, and it does include the second-order induction axiom, and it is still incomplete.

Therefore, the well-known categoricity proof must not rely solely on the second-order induction axiom. It also relies on a change to an entirely different semantics, apart from the choice of axioms. It is only in the context of these special "full" semantics that PA with the second-order induction axiom becomes categorical.

https://math.stackexchange.com/questions/617124/peano-arithm...

Thanks for the knoweledge. I'm going to read up more on this stuff.

Re: Fermat's Last Theorem – how it’s going

#187

Post by gedpeck »

Tainnor wrote: post #174
gedpeck wrote: post #170

Earlier quoted context omitted.

You know more than me. That is certain. However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this. If I take the standard model of ZFC and collect all true statements in the one model of PA_2 and make that my axiomatic system then I have an axiomatic system that is not recursively enumerable and contains PA_1. It’s not a nice se…

> However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this. That's a matter of semantics as to what you consider the first incompleteness theorem to be precisely (of which there are several variants). Gödel's proof itself doesn't directly work for second-order logic. But the statement "if Γ is some axiomatic system that satisfi…

From what you and the other person on this thread has said and from what I've read it appears that perhaps the following is true:

1. The axioms of PA_2 are recursively enumerable. 2. The full semantics of PA_2 are what cause categoricity.

It seems to me then that the crux of the matter is that the full semantics of PA_2 prevent there being an effective deductive system. I think Z_2 is constructed to get around the non effectiveness of the full semantics of PA_2 and is a weaker theory.

Anyway, thanks for the enlightenment.

Re: Fermat's Last Theorem – how it’s going

#188

Post by Tainnor »

gedpeck wrote: post #187
Tainnor wrote: post #174

Earlier quoted context omitted.

> However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this. That's a matter of semantics as to what you consider the first incompleteness theorem to be precisely (of which there are several variants). Gödel's proof itself doesn't directly work for second-order logic. But the statement "if Γ is some axiomatic system that satisfi…

From what you and the other person on this thread has said and from what I've read it appears that perhaps the following is true: 1. The axioms of PA_2 are recursively enumerable. 2. The full semantics of PA_2 are what cause categoricity. It seems to me then that the crux of the matter is that the full semantics of PA_2 prevent there being an effective deductive system. I think Z_2 is constructed to get around the no…

With the caveat that I don't really understand second order logic well enough to say all that much about it, there's a debate in the philosophy of mathematics as to whether second-order logic should count as the foundational logic, since on the one hand most first-order theories aren't categorical (due to Löwenheim-Skolem) and on the other hand, second order logic (with full semantics) already presupposes set theory.

In any case, the reason why PA_2 is categorical is because the second-order axiom of induction allows quantification over arbitrary sets which allows you to say that "0 and adding the successor function to 0 arbitrarily often already gives you all natural numbers".

Re: Fermat's Last Theorem – how it’s going

#189

Post by NL807 »

naasking wrote: post #155
mrintegrity wrote: post #146

Earlier quoted context omitted.

> The crowd went wild I am curious what a group of number theorists "going wild" looks like.. were they throwing chairs or are we talking slightly raised eyebrows?

Surely there was angry muttering.

Perhaps a chair tipped over at most.

Re: Fermat's Last Theorem – how it’s going

#190

Post by Tainnor »

naasking wrote: post #163
gedpeck wrote: post #132

Earlier quoted context omitted.

It shouldn’t and I didn’t say it should. I gave a fact and asked a question. Why is PA_2 computer science? Computer science ought to be about computation, right? There are non-computable objects that mathematicians study. Is that part of computer science?

> There are non-computable objects that mathematicians study. What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.

Constructivism is not mainstream mathematics.

The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to the axiom of choice, something that isn't valid in constructive logic. For many vector spaces you won't be able to write down a basis. And there are other examples, e.g. almost none of the automorphisms of C can be written down (only the identity and the conjugate map).

Post reply on HN