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

31–40 of 81 posts

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

#31

Post by adastra22 »

paulddraper wrote: post #19
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.

Yes and when it was first published it was wrong (made leap of logic). It takes thorough review by advanced mathematicians to verify correctness. This is not unlike a code review. Most people vastly underestimate how complex and esoteric modern research mathematics are.

The thing is though that MANY bugs slip through even the most thorough code reviews. As a security researcher, I can tell you there is literally no system out there that doesn't have such a bug in it.

The systems we deal with in software are massive compared with your typical mathematical framework though. But FLT is probably on similar scope.

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

#32

Post by adastra22 »

voxl wrote: post #25
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.

Why? Coding assistants tend to do even better in contexts where they have tools like type checkers and linters to verify their implementations. This area seems actually uniquely well suited to LLM usage.

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

#33

Post by rocqua »

adastra22 wrote: post #32
voxl wrote: post #25

Earlier quoted context omitted.

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.

Why? Coding assistants tend to do even better in contexts where they have tools like type checkers and linters to verify their implementations. This area seems actually uniquely well suited to LLM usage.

When I asked experts on formal proofs a year ago, their intuition was that there isn't enough formal proofs out there for LLMs to be very good at the syntax.

It's, as far as I know, quite hard to teach an LLM things it doesn't know.

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

#34

Post by yorwba »

adastra22 wrote: post #29
ethan_smith wrote: post #26

Earlier quoted context omitted.

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.

All three claims of gold medal performance on IMO 2025 that I'm aware of solved the first 5 problems, that were designed to be solvable by application of standard techniques, but got stumped on the sixth problem that was a bit more unusual. So it does seem like state-of-the-art models solve competition problems by recognizing which kind of problem it is and applying a corresponding solution template. Which is not too different from human competitors exploiting common question patterns, but humans seem to be able to degrade more gracefully by falling back to a more explorative mode when none of the standard tricks seem to apply.

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

#35

Post by Smaug123 »

mensetmanusman wrote: post #6

Are there any graphics that show the massive progress to date in some symbolic form?

There are 13 blueprint graphs (one for each chapter of the blueprint) so far, all incomplete. https://imperialcollegelondon.github.io/FLT/blueprint/dep_gr...

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

#36

Post by zozbot234 »

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…

Yup, Lean's quotient induction breaks subject reduction, which is an important type-theoretic principle. It means you can write a Lean development where t has type A, and t reduces (i.e. computes, as part of the Lean kernel) to u, but u doesn't have type A, and may not even type check. (See https://github.com/digama0/lean-type-theory/releases/downloa... Sec. 3.1 for a detailed discussion of this issue.) This is obviously quite bad, and it goes far beyond the usual drawback of adding axioms to a theory, including the quotient axiom. (Namely, the loss of canonicity.)

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

#37

Post by UltraSane »

voxl wrote: post #25
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.

Actually automated theorem provers like Lean are the PERFECT use for LLMs because you can instantly determine if the proof it generated is correct.

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

#38

Post by UltraSane »

rocqua wrote: post #33
adastra22 wrote: post #32

Earlier quoted context omitted.

Why? Coding assistants tend to do even better in contexts where they have tools like type checkers and linters to verify their implementations. This area seems actually uniquely well suited to LLM usage.

When I asked experts on formal proofs a year ago, their intuition was that there isn't enough formal proofs out there for LLMs to be very good at the syntax. It's, as far as I know, quite hard to teach an LLM things it doesn't know.

He is right and it doesn't matter because you can instantly tell if the proof the LLM generates is true or not.

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

#39

Post by staunton »

infogulch wrote: post #27
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.

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 unca…

Also a lot of errors would be called "typos", not errors. Such as some edge cases missing in the theorem statement which technically makes the theorem false. As long as there's a similar theorem in the same spirit that can be proven, that's what the original was all along.

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

#40

Post by ykonstant »

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…

> Kevin Buzzard told me that the worry that it might in fact be wrong is a huge motivator for him.

And then, when I raised concerns in Zulip about Lean's metaprogramming facilities being used to trick the pipeline into accepting false proofs, he said the opposite. He even emphasized that the formalization efforts are not for checking proof correctness, but for cataloguing truths we believe in.

This kind of equivocation turned me away from that community, to be honest. That was an extremely frustrating experience.

Post reply on HN