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

61–70 of 81 posts

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

#61

Post by tphyahoo2 »

CJefferson wrote: post #58
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.

I'm not disagreeing (I'm on the fence. Also a bit of a nube.). I thought this was a good read and on topic.

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

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

#62

Post by SabrinaJewson »

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…

It’s less nice from a computational perspective. But almost no mathematicians care about computation – they care about semantics, and there is no sense in which Lean’s quotients are a hack from a semantic perspective. I’m sure it makes computer scientists unhappy, but this isn’t a project for computer scientists.

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

#63

Post by mlyle »

matthewdgreen wrote: post #49
mlyle wrote: post #24

Earlier quoted context omitted.

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.

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

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

#64

Post by UltraSane »

wizzwizz4 wrote: post #57
UltraSane wrote: post #37

Earlier quoted context omitted.

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

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 absolutely not a normal or "not unusual" occurrence.

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

#65

Post by alphazard »

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.

This is an incredibly bad take on a hard social problem which is hard for reasons that are well understood.

Scientific research is often not immediately applicable, but can still be valuable. The number of people that can tell you if it's valuable are small, and as our scientific knowledge improves, the number of people who know what's going on shrinks and shrinks.

Separately, it's possible to spend many years researching something, and have very little to show for it. The scientists in that situation also want some kind of assurance that they will be able to pay their bills.

Between the high rate of failure, and conflicts of interest, and inscrutability of the research topics. It's very hard to efficiently fund science, and all the current ways of doing it are far from optimal. There is waste, there is grift, there is politics. Any improvement here is welcome, and decreasing the dollar cost per scientific discovery is more important than the research itself in any single field.

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

#66

Post by ants_everywhere »

SabrinaJewson wrote: post #62
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…

It’s less nice from a computational perspective. But almost no mathematicians care about computation – they care about semantics, and there is no sense in which Lean’s quotients are a hack from a semantic perspective. I’m sure it makes computer scientists unhappy, but this isn’t a project for computer scientists.

This article is about a team of mathematicians digitizing a proof that will take several years to realize. Lean itself is about computation.

So all the libraries they build up will have these holes in them that make it harder to do things like treat two isomorphic objects as the same -- something mathematicians do implicitly on a daily basis.

You can probably get a long way in Lean with the soundness axiom. But what I don't know is what happens when you build up a decade of software libraries in a system that adds a lot of manual and cognitive overhead when you want to use them.

My gut instinct is that by cutting corners now, they're creating a form of technical debt that could possibly escalate quickly and force mathematicians to reformulate their tools in a nicer way.

This actually happens continuously throughout the history of math. Sometimes it leads to errors like the so-called Italian school of algebra. Sometimes it just leads to pauses while we go back and figure out what the objects we're working with actually are before we can make more progress.

Take all this with a grain of salt: I haven't worked with Lean so I don't know how much this crops up in practice, and I don't know how large Lean libraries are at this point. This is all gut feeling.

But my sense is that what you really want is to get the foundations right, then build abstraction layers on those foundations that are nicer to use. Lean tries to build a "good enough" foundation and historically the gap between what we know is correct and what is seen to be "good enough" tends to show itself sooner or later in math. If you are just working in natural language then you can just forget it was a problem as soon as a fix is found. If you're working in software, though, you'll likely need to do a major rewrite or refactoring.

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

#67

Post by NooneAtAll3 »

jhanschoo wrote: post #28
amelius wrote: post #2

Since 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?

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

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

#68

Post by BoiledCabbage »

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.

I have little knowledge in this area, but my understanding is it's like this:

There is a pseudocode app that depends on a bunch of pseudocode libraries. They want to translate that pseudocode app into a real runnable app. They can do that, and it's a good amount of work, but reasonable. The problem is to get the app to run they also need to translate the hundreds or thousands of pseudocode libraries into actual libraries. Everything from OS APIs, networking libs, rendering libs, language standard libs all need ro be converted from specs and pseudocode to real code to actually run the app. And that's a ton of work.

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

#69

Post by kmill »

ants_everywhere wrote: post #66
SabrinaJewson wrote: post #62

Earlier quoted context omitted.

It’s less nice from a computational perspective. But almost no mathematicians care about computation – they care about semantics, and there is no sense in which Lean’s quotients are a hack from a semantic perspective. I’m sure it makes computer scientists unhappy, but this isn’t a project for computer scientists.

This article is about a team of mathematicians digitizing a proof that will take several years to realize. Lean itself is about computation. So all the libraries they build up will have these holes in them that make it harder to do things like treat two isomorphic objects as the same -- something mathematicians do implicitly on a daily basis. You can probably get a long way in Lean with the soundness axiom. But what…

> I haven't worked with Lean so I don't know how much this crops up in practice

It really doesn't. I've been using Lean and Mathlib for about five years now, and Fermat's Last Theorem is definitely not going to depend on the reduction properties of quotient types in the large scale.

Mathematical reasoning in Lean is almost universally done with rewriting, not reduction. People have found reduction based proofs (colloquially "heavy rfls") to be difficult to maintain. It exposes internal details of definitions. It's better to use the "public API" for mathematical definitions to be sure things can be refactored.

Really, quotients almost should never use the actual `Quot` type unless you have no better choice. In mathematics we like working with objects via universal properties ("public API"). A quotient type is any type that satisfies the universal property of a quotient. All `Quot` does is guarantee that quotients exist with reasonable computation properties, if we ever need them, and if we need those computation properties — which in the kind of math that goes into FLT we often don't. We don't even need `Quot` for Lean to have quotient types, since the classic construction of a set of equivalence classes works. (Though to prove that this construction is correct surely uses functional extensionality, which is proved using `Quot` in some way, but that's an implementation detail of `funext`.)

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

#70

Post by kmill »

amelius wrote: post #2

Since 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?

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

Post reply on HN