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

51–60 of 81 posts

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

#51

Post by cmrx64 »

semolinapudding wrote: post #43
cmrx64 wrote: post #23

Earlier quoted context omitted.

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.

Computation 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 reduc…

what does it mean to quotient datan’t?

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

#52

Post by tphyahoo2 »

"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")

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

#53

Post by enricozb »

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…

As 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.

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

#54

Post by gorkish »

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.

Unfortunately being noble or self righteous or whatever emotion you choose has nothing to do with it. If there is a pool of grant money available only to “Focused Research Organizations,” and you want some of it for your work, then you open one and do your work under that umbrella. Academic institutions themselves do this all the time. It looks politically and morally sketchy, and maybe it often is, but it’s the way it works.

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

#55

Post by wizzwizz4 »

bradly wrote: post #50
zozbot234 wrote: post #36

Earlier quoted context omitted.

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

Sorry if this is a silly question, but I came across a "white lie" in a paper( https://arxiv.org/html/2502.06137v2#S3.SS2 ) yesterday: > Throughout this section, we use A≈B to mean that A and B are essentially equal, in the sense that B is a suitable approximation of A in some sense that we will formalize in a later section. The reader may feel free to assume A=B when verifying estimates, even though A=B is generally…

No: you would want to formalise (or axiomatise) the notion of A≈B: assuming A=B when A≠B lets you prove basically whatever you like.

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

#56

Post by [deleted] »

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.

[deleted]

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

#57

Post by wizzwizz4 »

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.

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.)

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

#58

Post by CJefferson »

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…

I have no idea why Gemini is saying that. Proof my contradiction is totally fine. Sure, many people prefer a more direct proof as they are nicer to read, but proof by contradiction is totally fine and sometimes the only way to prove important results.

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

#59

Post by semolinapudding »

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.

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

#60

Post by lacker »

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…

By the time they are hoping to finish in 2029, I bet LLMs are capable of translating the proof from Lean into the alternate theorem proving language of your choice with only a small amount of human assistance.

If this does end up being the case, that translation becomes easy, then essentially all theorem proving efforts should be conducted in the language that is the easiest to work in. You can translate into the "mathematically superior" languages later.

Post reply on HN