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

11–20 of 81 posts

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

#11

Post by rcxdude »

amelius wrote: post #10
seanwilson wrote: post #9

Earlier quoted context omitted.

"The International Mathematical Olympiad (IMO) is the World Championship Mathematics Competition for High School students", so not to undermine it but it's below university or graduate level. Research level mathematics like this is as hard as it gets, and this proof is famously difficult: uses many branches of advanced mathematics, required thousands of pages of proofs, years of work.

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

No, some of the harder work has been done. Translating human-readable proofs into machine-readable ones is also very hard work and an area of active research.

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

#12

Post by seanwilson »

amelius wrote: post #10
seanwilson wrote: post #9

Earlier quoted context omitted.

"The International Mathematical Olympiad (IMO) is the World Championship Mathematics Competition for High School students", so not to undermine it but it's below university or graduate level. Research level mathematics like this is as hard as it gets, and this proof is famously difficult: uses many branches of advanced mathematics, required thousands of pages of proofs, years of work.

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 precisely traced back to axioms, handle all the edge causes, fix incorrect assumptions, and fill in the missing parts that were assumed to be straightforward but might not be.

A major part is you also have to formalise all the proofs your informal proof relied on so everything is traced back to the initial axioms e.g. you can't just cite Pythagorus theorem, you have to formalise that too.

So it's an order of magnitude more difficult to write a formal proof compared to an informal one, and even when you have the informal proof it can teams many years of effort.

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

#13

Post by bee_rider »

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…

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.

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

#14

Post by seanwilson »

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’m almost certain this is ignorance on my part, but it seems like this would mean the proof is… possibly wrong?

That's part of the motivation to formalise it. When a proof gets really long and complex, relies on lots of other complex proofs, and there's barely any single expert who has enough knowledge to understand all the branches of maths it covers, there's more chance there's a mistake.

There's a few examples here of errors/gaps/flaws found while formalizing proofs that were patched up:

https://mathoverflow.net/questions/291158/proofs-shown-to-be...

My understanding is it's common to find a few problems that then need to be patched or worked around. It's a little like wanting to know if a huge codebase is bug-free or not: you might find some bugs if you formalized the code, but you can probably fix the bugs during the process because it's generally correct. There can be cases where it's not fixable though.

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

#15

Post by 6gvONxR4sf7o »

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.

The level of rigor used in math if sometimes characterized as "sufficient to convince other mathematicians of correctness." So, yeah possibly, but not in a willy nilly way. It's not a proof sketch, it's a proof. It just isn't written in human language designed for communication.

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

#16

Post by williamstein »

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.

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 related quote Bryan Birch told me once: “it is always a good idea to prove true theorems.”

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

#17

Post by ants_everywhere »

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 nice from a mathematical perspective.

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

#19

Post by paulddraper »

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.

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.

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

#20

Post by YossarianFrPrez »

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://scienceplusplus.org/metascience/)

Post reply on HN