9 ms·
Ongoing Lean formalization of the proof for Fermat's Last Theorem
https://github.com/ImperialCollegeLondon/FLT/blob/main/GENERAL.md https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER...
- amelius 1y agoSince 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?
- tripplyons 1y agoYou're either underestimating the length of the proof, or overestimating the length of tasks that models can currently accomplish.
- amelius 1y agoThe blueprint is a step-by-step outline.
- tripplyons 1y agoIf the goal is to formalize the proof, you would need more than an outline.
- rcxdude 1y agoThis 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.
- Davidzheng 1y agoI disagree. I think it's a sequence of a huge number of modular moderately hard tasks each much easier than a hard IMO question.
- markusde 1y agoIMO 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.
- seanwilson 1y ago"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.
- amelius 1y agoYes but the hard work (coming up with a human-readable proof) has already been done.
- rcxdude 1y agoNo, 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.
- seanwilson 1y agoHuman 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.
- bee_rider 1y agoI’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.
- voxl 1y agoProof 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.
- adastra22 1y agoWhy? 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.
- rocqua 1y agoWhen 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.
- UltraSane 1y agoHe is right and it doesn't matter because you can instantly tell if the proof the LLM generates is true or not.
- deleted 1y ago[deleted]
- kmill 1y agoI 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.
- ethan_smith 1y agoFormalizing 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.
- adastra22 1y agoThat's not how state of the art models work.
- yorwba 1y agoAll 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.
- jhanschoo 1y agoIn addition to other comments, see https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/ 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.
- NooneAtAll3 1y ago> and my understanding of Maria Ines’ talk is that these issues have now been sorted out
- jhanschoo 1y agoI 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.
- kmill 1y agoMy understanding is that the proof doesn't exist in written form in its entirety. Plus, Kevin Buzzard is a world expert with some ideas for how to better organize the proof. In general, formalization leads to new understanding about mathematics. Something people outside of mathematics don't tend to appreciate is that mathematicians are usually thinking deeply about what we already know, and that work reveals new structures and connections that clarify existing knowledge. The new understanding reveals new gaps in understanding, which are filled in, and the process continues. It's not just about collecting verifiably true things. Even if somehow the OpenAI algorithm could apply here, we'd get less value out of this whole formalization exercise than to have researchers methodically go through our best understanding of our best proof of FLT again.
- seanwilson 1y agoThis is a nice overview of what this is, why they're doing it and why it's many years of work: https://github.com/ImperialCollegeLondon/FLT/blob/main/GENERAL.md https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER...
- dang 1y agoLink added to top text. Thanks!
- mensetmanusman 1y agoAre there any graphics that show the massive progress to date in some symbolic form?
- Smaug123 1y agoThere are 13 blueprint graphs (one for each chapter of the blueprint) so far, all incomplete. https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_chapter_13.html https://imperialcollegelondon.github.io/FLT/blueprint/dep_gr...
- ants_everywhere 1y agoI 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.
- cmrx64 1y agoWhat’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.
- semolinapudding 1y agoComputation is the difference. In Lean, applying the universal property of the quotient (`Quotient.lift f Hf`) to an element that is of the form `Quotient.mk a` reduces to `f a`. This rule is fine in itself, but the Lean developers were not sufficiently careful and allowed it to apply for quotients of propositions, where it interferes with the computation rules for proof irrelevance and ends up breaking subject reduction (SR is deeply linked to computation when you have dependent types!) [0]. It is not really a problem in practice though, since there is no point in quotienting a proposition. [0] see the end of section 3.1 in https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf https://github.com/digama0/lean-type-theory/releases/downloa...
- cmrx64 1y agowhat does it mean to quotient datan’t?
- zozbot234 1y agoYup, 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/download/v1.0/main.pdf 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.)
- YossarianFrPrez 1y agoSide 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 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/ https://scienceplusplus.org/metascience/)
- pierrefermat1 1y agoThe 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.
- mlyle 1y agoTo 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.
- matthewdgreen 1y agoHaving an organization maintain a software tool seems pretty unsurprising. There’s a well-defined problem with easily visible deliverables, relatively little research risk, and small organizations routinely maintain software tools all the time. Whereas broader research is full of risk and requires funders be enormously patient and willing to fund crazy ideas that don’t make sense.
- mlyle 1y agoHmm. I don't know very much about Lean, and it definitely feels smaller in scope and coordination risk than the kinds of things that would generally benefit from this. (OTOH, within the community they're effectively trying to build a massive, modern Principia Mathematica, so maybe they would...) > Whereas broader research is full of risk and requires funders be enormously patient and willing to fund crazy ideas that don’t make sense. Yah. I'm not a researcher, but I keep ending up tangentially involved in research communities. I've seen university labs, loose research networks, loose consortia funding research centers, FFRDC, etc. What I’ve noticed is that a lot of these consortia or networks struggle to deliver anything cohesive. There's too many stakeholders, limited bandwidth, and nobody quite empowered to say “we’re building this.” In the cases where there’s a clearly scoped, tractable problem that’s bigger than what a single lab can handle, and a group of stakeholders agrees it’s worth a visionary push, something like an FRO might make a lot of sense.
- tphyahoo2 1y ago"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_proof_of_Fermat%27s_Last_Theorem So, will the Lean formalization of FLT involve translation to a direct or constructive proof? It seems not, I gather the proof will rely on classical not constructive logic. "3. Proof by Contradiction: The core of the formal proof involves assuming ¬Fermat_Last_Theorem and deriving a contradiction. This contradiction usually arises from building a mathematical structure (like an elliptic curve) based on the assumed solution and then demonstrating that this structure must possess contradictory properties, violating established theorems. 4. Formalizing Contradiction: The contradiction is formalized in Lean by deriving two conflicting statements, often denoted as Q and ¬Q, within the context of the assumed ¬Fermat_Last_Theorem. Since Lean adheres to classical logic, the existence of these conflicting statements implies that the initial assumption (¬Fermat_Last_Theorem) must be false." (gemini llm answer to google query: Lean formalization of fermat's last theorem "proof by contradiction")
- enricozb 1y agoAs far as I understand, The lead of this project Kevin Buzzard is a mathematician first. And the majority of mathematicians are untroubled by non-constructive proofs. I would imagine that proof directions that result in the most interesting additions to Mathlib would be chosen.
- semolinapudding 1y agoFLT 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.
- bananaflag 1y agoA purely universal statement, to be more clear.