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

Ongoing Lean formalization of the proof for Fermat's Last Theorem

github.com

Post reply on HN
Print view View original

21–30 of 81 posts

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#21

Post by pierrefermat1 »

YossarianFrPrez wrote: post #20

Side note: The organization that maintains Lean is a "Focused Research Organization", which is a new model for running a science/discovery based nonprofit. This might be useful knowledge for founder types who are interested in research. For more information, see: https://www.convergentresearch.org And if you want to read why we need additional types of science organizations, see "A Vision of Metascience" ( https://sc…

The concept trying new science orgs is noble, but this is the typical Schmidt BS of saying every previous academic consortia is totally incompetent and I'm the only one that can inject the magic sauce of focus and coordination.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#22

Post by Davidzheng »

rcxdude wrote: post #8
amelius wrote: post #2

Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?

This is a significantly harder problem than winning gold in IOM. A large part of it is figuring out how to represent some of the relevant ideas in Lean at all.

I disagree. I think it's a sequence of a huge number of modular moderately hard tasks each much easier than a hard IMO question.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#23

Post by cmrx64 »

ants_everywhere wrote: post #17

I love that they want to formalize this proof, and I understand why they're using Lean. But part of me feels like if they are going to spend the massive effort to formalize Fermat's Last Theorem it would be better to use a language where quotient types aren't kind of a hack. Lean introduces an extra axiom as a kind of cheat code to make quotients work. That makes it nicer from a softer dev perspective but IMO less ni…

What’s mathematically questionable about the quotient soundness axiom? It’s justifiable metamathematically. What’s the real difference baking it into the proof kernel? I’d rather such independent properties be modeled as an axiom. The quotient automation I’m familiar with in other theorem provers is typically way more (untrusted!) machinery than just stating quot.sound.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#24

Post by mlyle »

pierrefermat1 wrote: post #21
YossarianFrPrez wrote: post #20

Side note: The organization that maintains Lean is a "Focused Research Organization", which is a new model for running a science/discovery based nonprofit. This might be useful knowledge for founder types who are interested in research. For more information, see: https://www.convergentresearch.org And if you want to read why we need additional types of science organizations, see "A Vision of Metascience" ( https://sc…

The concept trying new science orgs is noble, but this is the typical Schmidt BS of saying every previous academic consortia is totally incompetent and I'm the only one that can inject the magic sauce of focus and coordination.

To me, it seems like coming up with something more coordinated than a consortium and more flexible than a single lab or a research corporation funded by multiple universities makes sense.

It's probably a narrow set of problems with the right set of constraints and scale for this to be a win.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#25

Post by voxl »

amelius wrote: post #2

Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?

Proof assistant code is high reliability, there is no room to fudge it. This is perhaps the one place where you can really see how bad LLMs are when you care about reliability.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#26

Post by ethan_smith »

amelius wrote: post #2

Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?

Formalizing Wiles' proof requires translating hundreds of pages of sophisticated mathematics with implicit reasoning steps into a precise logical framework, which is fundamentally different from the pattern-matching AI uses to solve competition problems.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#27

Post by infogulch »

bee_rider wrote: post #13
seanwilson wrote: post #12

Earlier quoted context omitted.

Human readable (informal) proofs are full of gaps that all have to be traced back to axioms e.g. gaps that rely on shared intuition, background knowledge and other informal proofs. It's somewhat like taking rough pseudo code (the informal proof, a mixture of maths and English) and translating that into a bullet-proof production app (the formal proof, in Lean), where you're going to have to specify every step precisel…

I’m almost certain this is ignorance on my part, but it seems like this would mean the proof is… possibly wrong? I mean if there are gaps and other informal proofs in there? But I thought it was a widely celebrated result.

I think it was Terrance Tao on the Lex Friedman podcast recently that said that there are very often little mistakes in big proofs, but they are almost always able to be patched around. Its like mathematicians' intuition is tracking some underlying reality and the actual formalization is flexible. Yes sometimes digging down into a small mistake leads to an unbridgeable gap and that route has to be abandoned, but uncannily often such issues have nearby solutions.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#28

Post by jhanschoo »

amelius wrote: post #2

Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?

In addition to other comments, see https://xenaproject.wordpress.com/2024/12/11/fermats-last-th...

In particular, note that a key lemma of crystalline cohomology rests on a mistake. Experts think that it is fixable by virtue that results have depended on it for a long time and no issue was found, but it is not fixed.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#29

Post by adastra22 »

ethan_smith wrote: post #26
amelius wrote: post #2

Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?

Formalizing Wiles' proof requires translating hundreds of pages of sophisticated mathematics with implicit reasoning steps into a precise logical framework, which is fundamentally different from the pattern-matching AI uses to solve competition problems.

That's not how state of the art models work.

Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem

#30

Post by adastra22 »

williamstein wrote: post #16
bee_rider wrote: post #13

Earlier quoted context omitted.

I’m almost certain this is ignorance on my part, but it seems like this would mean the proof is… possibly wrong? I mean if there are gaps and other informal proofs in there? But I thought it was a widely celebrated result.

Kevin Buzzard told me that the worry that it might in fact be wrong is a huge motivator for him. I also once asked Serge Lang why so much mathematics is correct (which surprised me coming from programming where everything has bugs), and he said; “people do a large number of consistency checks beyond what is in the published proofs, which makes the chances the claimed results are correct much, much higher.” Another re…

I suspect he is massively overestimating the reliability of obscure mathematics.
Post reply on HN