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

41–50 of 81 posts

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

#41

Post by Gehinnn »

zozbot234 wrote: post #36
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 obvio…

How much does this leak into typical math-related proofs? If someone would create LeanQ where quotient types are built in nicely, how much work would it be to port the Fermat project from Lean to LeanQ?

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

#42

Post by zozbot234 »

Gehinnn wrote: post #41
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…

How much does this leak into typical math-related proofs? If someone would create LeanQ where quotient types are built in nicely, how much work would it be to port the Fermat project from Lean to LeanQ?

AIUI, this cannot lead to inconsistency or a "wrong" proof. So if a proof checks out in Lean that's good enough, you might not even need a separate LeanQ.

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

#43

Post by semolinapudding »

cmrx64 wrote: post #23
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…

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 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/downloa...

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

#44

Post by semolinapudding »

Gehinnn wrote: post #41
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…

How much does this leak into typical math-related proofs? If someone would create LeanQ where quotient types are built in nicely, how much work would it be to port the Fermat project from Lean to LeanQ?

AFAICT, this issue only comes up if you form the quotient of a proposition by a relation. But there is no point in doing that (all the proofs of a proposition are already equal!) so it's not an issue in practice and it wouldn't be difficult to fix.

However, Lean's SR is broken in other ways which do show up in practice: definitional proof irrelevance is incompatible with Lean's computation rule for Acc. That one is much harder to fix.

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

#45

Post by semolinapudding »

ykonstant wrote: post #40
williamstein wrote: post #16

Earlier quoted context omitted.

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

For what it's worth, I don't think that Kevin Buzzard is the person you should talk to if you are interested in proof assistant design. As far as I know, Buzzard does not consider himself to be an expert in type theory or in proof assistants, and claims to be a mere user.

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

#46

Post by Gehinnn »

zozbot234 wrote: post #42
Gehinnn wrote: post #41

Earlier quoted context omitted.

How much does this leak into typical math-related proofs? If someone would create LeanQ where quotient types are built in nicely, how much work would it be to port the Fermat project from Lean to LeanQ?

AIUI, this cannot lead to inconsistency or a "wrong" proof. So if a proof checks out in Lean that's good enough, you might not even need a separate LeanQ.

Does this mean that most of the proofs in Lean and LeanQ would look exactly the same, it's just that the proofs of some technical low-level lemmas around quotient types (which I guess mathematicians are not really interested in anyway) look different?

For example, if I want to prove that a+b=b+a, I wouldn't care if I'm directly in peano arithmetic or just have a construction of the peano axioms in ZFC, as in both cases the proofs would be identical (some axioms in PA would be lemmas in ZFC).

If that's the case with quotients, I wonder why it's such a big deal for some.

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

#47

Post by seanwilson »

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…

> “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.”

I imagine one bias is because formal verification is such a huge effort, you're only going to do it for really interesting and impactful proofs, which means the proofs that get formal verified will already have been reviewed and critiqued a lot, and will be less likely to have glaring critical errors.

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

#48

Post by griffzhowl »

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.

The problem is if they don't produce any correct ones then that doesn't matter

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

#49

Post by matthewdgreen »

mlyle wrote: post #24
pierrefermat1 wrote: post #21

Earlier quoted context omitted.

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.

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

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

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

#50

Post by bradly »

zozbot234 wrote: post #36
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 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 false.

Is that when this would be needed?

Post reply on HN