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

161–170 of 216 posts

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

#161

Post by naasking »

coliveira wrote: post #6
seanwilson wrote: post #5

> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. 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. For me, this is just…

> 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.

> So this points to a fundamental problem with using AI to do math.

No it doesn't, AI like an LLM has no issues with stating two inconsistent propositions, just like humans, which is why both AI and humans can reason about all of mathematics, eg. Godel theorems is that a formal system cannot simultaneously be complete and consistent.

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

#162

Post by naasking »

pkoird wrote: post #21
dboreham wrote: post #16

Earlier quoted context omitted.

And Mathematics is Computer Science. Took me most of a lifetime to realize this.

I'd argue for the converse: Computer Science is Mathematics

> I'd argue for the converse: Computer Science is Mathematics

The space of programs is arguably larger than the space of mathematical systems, because programs can be logically inconsistent. This suggests that mathematics is a logically consistent subset of computer science, not the other way around.

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

#163

Post by naasking »

gedpeck wrote: post #132
immibis wrote: post #100

Earlier quoted context omitted.

why should computer science be limited to things that are first order PA?

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.

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

#164

Post by gedpeck »

semolinapudding wrote: post #150
gedpeck wrote: post #131

Earlier quoted context omitted.

Do you have a reference for the second order induction schema being recursively enumerable? My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable. The second order Axioms are different than second order Arithmetic. https://mathoverflow.net/questions/97077/z-2-versus-second-o.…

If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the second-order induction axiom (in your first mathoverflow link, this is called Z_2): https://en.wikipedia.org/wiki/Second-order_arithmetic#The_fu... An other equivalent option would be to use the language…

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 know if computably enumerable is the same as recursively enumerable but given what you’ve said I’m guessing they are different notions.

Consider the standard model of ZFC. Assume ZFC is consistent. Within this model there is one model of PA_2. Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.

Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.

If those axioms were recursively enumerable then the Incompleteness theorems would apply, right?

What Noah Schweber says here seems pertinent:

https://math.stackexchange.com/questions/4972693/is-second-o...

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

#165

Post by boothby »

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.

Multiple people raising objections at once, each at a reasonable volume to speak to a large seminar room, and other people speaking to their immediate neighbor. If there was angry muttering, I don't recall it. But yes, a crowd of mathematicians going wild is still pretty chill.

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

#166

Post by gedpeck »

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.

The set of statements about natural numbers that are true.

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

#167

Post by digama0 »

Retr0id wrote: post #17

This makes me wonder if there'll ever be a significant bug discovered in Lean itself, breaking past formalisation work.

Fun fact, there have been 3 soundness bugs in lean 4 so far. (They were all fixed within hours.) I expect we have not yet found them all, but I also do not sleep poorly worried that mathematics will come tumbling down, because these are invariably implementation bugs (either in the literal sense of implementation of the system, or in the implementation of mathematics in the type theory). If something is wrong it is almost certainly going to be the system and not the mathematics. But I'm saying this as someone who works on the proof assistant itself (i.e. hold fixed the mathematics, vary the proof assistant). Kevin Buzzard will say the exact opposite because he is working on the mathematics (vary the mathematics, hold fixed the proof assistant), in which case the likely failure modes will be that a given proof is written poorly, a definition has incorrect behavior on edge cases, etc, but only the current proof is under threat, not some completely unrelated e.g. proof of infinitude of primes deep in the library.

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

#168

Post by Tainnor »

gedpeck wrote: post #159
Tainnor wrote: post #152

Earlier quoted context omitted.

> My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable Incompleteness does apply to second order arithmetic (it applies to every logical system that contains first order PA), but due to different reasons: second order logic doesn't have a complete proof calculus. "Second-ord…

I think you are wrong in your first sentence. Take the collection of all true statements and make that your axiomatic system. Andreas Blass in the comments says that Incompleteness does not apply to PA_2. https://math.stackexchange.com/questions/4753432/g%C3%B6dels...

> Take the collection of all true statements and make that your axiomatic system.

A complete proof system needs to be able to derive Γ |- φ for every pair Γ, φ such that Γ |= φ. Not just when Γ is the complete theory of some structure. Completeness of first-order logic (and its failure for second-order logic) is about the logical system itself, while the incompleteness theorems are about specific theories - people often mix these up, but they talk about very different things.

> Andreas Blass in the comments says that Incompleteness does not apply to PA_2.

He says something rather different, namely that its "meaningless". That's a value judgement. Incomplete proof calculi for second order logic do exist (e.g. any first-order proof calculus) and for those, what I wrote is true. Andreas Blass would probably just think of this as an empty or obvious statement.

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

#169

Post by nicf »

bandrami wrote: post #128
impendia wrote: post #48

Earlier quoted context omitted.

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone w…

Is there really not a centralized corpus of that kind of fundamental result you guys can use? I would have assumed that was "theorem #44756" in a giant tome you all had in your bookshelf somewhere.

Nope. Many important results have names that are familiar to everyone in the subfield, so you might say "by So-and-So's Lemma, this module is finitely generated". Failing that, you could maybe cite a paper or a book where the result appears, like "We can then conclude using Corollary 14.7 from [31] that...", where [31] is in your bibliography.

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

#170

Post by gedpeck »

Tainnor wrote: post #168
gedpeck wrote: post #159

Earlier quoted context omitted.

I think you are wrong in your first sentence. Take the collection of all true statements and make that your axiomatic system. Andreas Blass in the comments says that Incompleteness does not apply to PA_2. https://math.stackexchange.com/questions/4753432/g%C3%B6dels...

> Take the collection of all true statements and make that your axiomatic system. A complete proof system needs to be able to derive Γ |- φ for every pair Γ, φ such that Γ |= φ. Not just when Γ is the complete theory of some structure. Completeness of first-order logic (and its failure for second-order logic) is about the logical system itself, while the incompleteness theorems are about specific theories - people of…

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 set of axioms. It’s not computable. But it shows that one can have an axiomatic system that contains PA_1 for which the Incompleteness theorems don’t apply.

Andreas wrote “meaningless” not “nonsensical”. I’m not a pedant but the former term evokes in me the idea of “does not apply in this situation becausethe hypotheses of the incompleteness theorem are not satisfied”.

From a mathematical logic book is the following. It’s the set up for the Incompleteness theorems.

Suppose that A is a collection of axioms in the language of number theory such that A is consistent and is simple enough so that we can decide whether or not a given formula is an element of A.

PA_2 is not such a system and as such the Incompleteness Theorems don’t apply. Maybe we are talking past each other. You know more than me.

Post reply on HN