Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Formalizing Fermat's Last Theorem

anthropic.com

Post reply on HN
Print view View original

401–410 of 524 posts

Re: Formalizing Fermat's Last Theorem

#401

Post by Smaug123 »

jmusall wrote: post #204
Smaug123 wrote: post #110

Earlier quoted context omitted.

It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.

The comparator was only used to verify that the final statement indeed is a valid formalization of Fermat's Last Theorem, not that the proof leading up to it is correct.

I think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.

Re: Formalizing Fermat's Last Theorem

#402

Post by marwahaha »

mikmoila wrote: post #196

"The effort succeeded when we switched to using Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University." So in the end, it required tooling crafted by humans.

I was involved in building https://prove2.me (but I am not affiliated with Anthropic nor involved in anything related to FLT). I think the key insight in prove2me is to prove theorems "top-down", which allows a large number of users to collaboratively work on a single theorem statement. This setup also seems to work well for a "swarm" of agents. I posted more of my thoughts on the Lean Zulip.

Re: Formalizing Fermat's Last Theorem

#403

Post by Smaug123 »

andriy_koval wrote: post #291
Almondsetat wrote: post #287

Earlier quoted context omitted.

and you are entitled to talk about maths while rejecting maths

coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants. I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet,…

Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.

Re: Formalizing Fermat's Last Theorem

#404

Post by Smaug123 »

andriy_koval wrote: post #332
drdeca wrote: post #325

Earlier quoted context omitted.

ZFC has greater consistency strength than PA. If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.

zfc doesn't have functions, so you are building something new on top of it. Also, I am not sure successor function is enough for PA.

It simply does have functions. According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element.

I mean this quite seriously: have you considered reading any first course in set theory?

Re: Formalizing Fermat's Last Theorem

#405

Post by marwahaha »

kzrdude wrote: post #40

The part about prove2.me was interesting. That means that a co-working tool was instrumental in the project, and I think AI companies will take note of this. Is this proof specific or will we need to give agents access to JIRA or similar tools to solve large projects in the future?

I helped build https://prove2.me . It's not proof-specific but everything is Lean-based. I've found the tool useful when formalizing recent upper bounds on $\omega$ (in computational complexity of matrix multiplication). A lot of ideas in this tool are experimental, but the intent is to benefit the mathematical community at large. I'd be happy to hear about any suggestions or advice others have.

Re: Formalizing Fermat's Last Theorem

#406

Post by IsTom »

andriy_koval wrote: post #259
IsTom wrote: post #245

Earlier quoted context omitted.

> Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC. https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...

> interpreted its hard to me to tell what this means formally(as I said I am not expert). There is no "interpret" operator in zfc. I believe what it says if you add some robinson axioms + some logical rules on top of zfc, you can carry your results.

It's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given.

You don't need to add any axioms, you just build some sets to represent numbers and make operations that act the same way as arithmetic, define some equality relations. Then you derive rules of arithmetic for your handcrafted arithmetic using ZF axioms and you're good. You get axioms of arithmetic derived from your regular axioms without adding them as new axioms to your theory.

Re: Formalizing Fermat's Last Theorem

#407

Post by throw-qqqqq »

twiceaday wrote: post #351
herbcso wrote: post #350

So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…

Lean is like a statically typed programming language and validity is guaranteed if it compiles. The only room for errors is in translating a non-Lean theorem into Lean, so that you are not proving what you think you are proving.

Great explanation. I’ve heard this referred to, as The Formal Specification problem.

From https://en.wikipedia.org/wiki/Formal_specification#Limitatio...

> A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “correct with respect to a given specification.” Whether the formal specification correctly describes the problem to be solved is a separate issue.

Re: Formalizing Fermat's Last Theorem

#408

Post by Smaug123 »

andriy_koval wrote: post #208
ajs1998 wrote: post #140

Earlier quoted context omitted.

ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.

do we know if claude's formalization is built on top of zfc and not zfc+extra? zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.

Claude’s formalisation, being in Lean, is based on the calculus of inductive constructions, not ZFC. In Lean 3, per Carneiro, any theorem of Lean 3’s theory can be proved in ZFC plus some finite number of inaccessible cardinals (and, IIRC, vice versa). The precise strength of Lean 4 is not quite clear yet, I think (I guess this is partly what Lean4Lean is hoping to address).

Re: Formalizing Fermat's Last Theorem

#409

Post by throw-qqqqq »

throw567643u8 wrote: post #379
herbcso wrote: post #350

So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…

With the size of the proof object, a potential buffer overflow comes to mind.

Buffer overflows are trivial to check for at runtime (~proof-checking-time) and Lean does this. Just like Java does it.

I’d wager a million gazillion bucks that this is not the case.

Re: Formalizing Fermat's Last Theorem

#410

Post by qnleigh »

lalitmaganti wrote: post #3

I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment, what it means but also doesn't mean.

I wonder what he's feeling about this. Formalizing Fermat's last theorem was a huge undertaking, and has been a big part of his career for some time. Now the announcement has been made, and even if there is more work that he wants to do, he has in some ways been scooped by an LLM.

Fortunately he is a very well-established mathematician, so career-wise he will likely be fine. But if an early-career mathematician gets scooped this badly it could be career-ending.

Post reply on HN