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

71–80 of 81 posts

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

#71

Post by kmill »

UltraSane wrote: post #38
rocqua wrote: post #33

Earlier quoted context omitted.

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.

I see people on Zulip using Copilot to write Lean proofs, and they have some success, but the quality is really bad right now, creating long, unmaintainable proofs. New users get stuck, thinking they're 90% of the way to the end, but really the whole thing probably should be scrapped and they should start over.

It's a bit frustrating because, before Copilot, new users would come with proofs and you could spend some time helping them write better proofs and they'd learn things and gain skills, but now it's not clear that this is time well spent on my part. Copilot is not going to learn from my feedback.

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

#72

Post by amelius »

seanwilson wrote: post #12
amelius wrote: post #10

Earlier quoted context omitted.

Yes but the hard work (coming up with a human-readable proof) has already been done.

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…

> It's somewhat like taking rough pseudo code and translating that into a bullet-proof production app

That's actually where LLMs are already quite good at.

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

#73

Post by oasisaimlessly »

amelius wrote: post #72
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…

> It's somewhat like taking rough pseudo code and translating that into a bullet-proof production app That's actually where LLMs are already quite good at.

/s

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

#74

Post by bananaflag »

semolinapudding wrote: post #59
tphyahoo2 wrote: post #52

"In constructive mathematics, proof by contradiction, while not universally rejected, is treated with caution and often replaced with direct or constructive proofs." (gemini llm answer to google query: constructive math contradiction) "Wiles proved the modularity theorem for semistable elliptic curves, from which Fermat’s last theorem follows using proof by contradiction." https://en.wikipedia.org/wiki/Wiles%27s_proo…

FLT is a negative statement ("there are no nonzero integers x, y, z such that..."), and proofs by contradiction are constructively valid for proving negative statements.

A purely universal statement, to be more clear.

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

#75

Post by jhanschoo »

NooneAtAll3 wrote: post #67
jhanschoo wrote: post #28

Earlier quoted context omitted.

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.

> and my understanding of Maria Ines’ talk is that these issues have now been sorted out

I think you are trying to say that this matter has since been resolved and so presumably the whole informal proof somehow resides in literature. I suppose that to the first point you may be right (I'm guessing that it's since been made available), but to the second point I think you are overconfident that similar gaps do not exist.

I admit that my original comment was inaccurate, as it seems to suggest that the gap still exists.

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

#76

Post by markusde »

Davidzheng wrote: post #22
rcxdude wrote: post #8

Earlier quoted context omitted.

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.

IMO problems are stated in and solved by math a high schooler could understand. Getting the definitions right (one of the harder parts of mechanizing proofs IME) is a different beast altogether.

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

#77

Post by markusde »

UltraSane wrote: post #37
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.

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

Proofs, sure, but not definitions. A human needs to be sure that the definitions align with that they expect. Unfortunately, humans generating correct definitions and LLM's generating correct proofs are not independent problems.

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

#78

Post by wizzwizz4 »

UltraSane wrote: post #64
wizzwizz4 wrote: post #57

Earlier quoted context omitted.

Actually , some proofs take longer for the computer to verify than for a human (even an unskilled typist) to type out. Several hours to evaluate a two-page document isn't unusual. (I prefer to write optimised proofs, but it can take me weeks to find the correct abstractions for that.)

Are you talking about Lean 4? Lean 4 is usually pretty fast at verifying proofs and most proofs are created in interactive mode so are checked as they are typed. A "two-page document" (perhaps 200-300 lines of code) would typically check in a matter of seconds to, at most, a few minutes. If it took hours, it would mean the file contains a pathological case that a developer would be expected to identify and fix. It is…

Steps to reproduce:

1. Load a complex data structure, e.g. from JSON. (I do not consider typing out the JSON to be part of the human's job.)

2. Process the data, using the magic of functional programming. (Performance? What's that? Performance is not a priority.)

3. Add some helpful lemmas.

4. Prove the data processing stage was correct… but proving this in general is haaaard, so just make automation that's capable of proving it for most cases… eventually.

5. Great! It takes 3 minutes to run on my tiny examples. Now run it on the real data.

And that's where hours come from!

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

#79

Post by UltraSane »

wizzwizz4 wrote: post #78
UltraSane wrote: post #64

Earlier quoted context omitted.

Are you talking about Lean 4? Lean 4 is usually pretty fast at verifying proofs and most proofs are created in interactive mode so are checked as they are typed. A "two-page document" (perhaps 200-300 lines of code) would typically check in a matter of seconds to, at most, a few minutes. If it took hours, it would mean the file contains a pathological case that a developer would be expected to identify and fix. It is…

Steps to reproduce: 1. Load a complex data structure, e.g. from JSON. (I do not consider typing out the JSON to be part of the human's job.) 2. Process the data, using the magic of functional programming. (Performance? What's that? Performance is not a priority.) 3. Add some helpful lemmas. 4. Prove the data processing stage was correct… but proving this in general is haaaard, so just make automation that's capable o…

This is NOT what Lean 4 is designed to do. You seem to be using Lean 4 for what TLA+ is much better suited for.

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

#80

Post by tphyahoo2 »

semolinapudding wrote: post #59
tphyahoo2 wrote: post #52

"In constructive mathematics, proof by contradiction, while not universally rejected, is treated with caution and often replaced with direct or constructive proofs." (gemini llm answer to google query: constructive math contradiction) "Wiles proved the modularity theorem for semistable elliptic curves, from which Fermat’s last theorem follows using proof by contradiction." https://en.wikipedia.org/wiki/Wiles%27s_proo…

FLT is a negative statement ("there are no nonzero integers x, y, z such that..."), and proofs by contradiction are constructively valid for proving negative statements.

Thanks for articulating this.

https://math.andrej.com/2010/03/29/proof-of-negation-and-pro...

also

"It’s fine to use a proof by contradiction to show something doesn’t exist. When the assumption that it does exist leads to a contradiction, then that shows it can’t exist.

It’s not so fine to use a proof by contradiction to show something does exist. Here’s the situation. The assumption that it does not exist leads to a contradiction. What can you conclude from that? You would like say “therefore it exists”. But you haven’t got any idea what it is. You may know it’s out there somewhere, but you have no idea how to find it. It would be better to have a proof that tells you what it is.

That’s a difference between what’s called “classical logic” and “intuitionistic logic”. In classical logic, proof by contradiction is perfectly accepted as a method of deductive logic. In intuitionistic logic, proof by contradiction is accepted to show something doesn’t exist, but is not accepted to show something does exist."

David Joyce, https://www.quora.com/In-math-are-there-any-proofs-that-can-...

Post reply on HN