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

441–450 of 531 posts

Re: Formalizing Fermat's Last Theorem

#441

Post by kzrdude »

stratos123 wrote: post #71
hyperhello wrote: post #53

Earlier quoted context omitted.

The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled. Note to other users: don’t downvote this kind of comment, answer it.

encode mathematical reasoning in a way that can’t be fooled. I would be a bit careful asserting that in full generality, given https://github.com/James-Hanson/junk-theorems-in-lean

Some kind of linter should flag these with a warning, I think

Re: Formalizing Fermat's Last Theorem

#442

Post by lukewarm707 »

CaptWorld wrote: post #388
lukewarm707 wrote: post #306

Earlier quoted context omitted.

a) classic goodhart is using gdp as a measure of prosperity. the government sets a prosperity target. to increase prosperity the government makes workers increase gdp by working 16 hours per day. gdp increases. prosperity is up! the metric is now poisoned. b) how and why could human welfare get worse in a growing economy, really the list is long. one example, unsustainable industries grow but do not create surplus. t…

A) that's a bad model to think. You are of the mind that working more hours is the only way to measure gdp whereas increase in productivity with tools like AI, machinery, tech etc can act as a multiplier. So this way you are conflating bad ways to increase gdp with good ways like AI. That's how US is powerhouse as they are basically a technological hub of the world. B) ha? More fish means couple of things.. they're a…

i can agree with some of this but you are missing the point about the fish. the catch grows year on year. however the fish stock is depleted at a faster rate than it is replenished. it is unsustainable. the catch reaches a maximum and starts to decline as they run out of fish.

it is not really creating wealth, it is destroying existing wealth. it is destroying the productive ecosystem. the future population will be poorer for having lost this productive asset.

Re: Formalizing Fermat's Last Theorem

#443

Post by dahart »

salomonk_mur wrote: post #132
t_gamer_kle wrote: post #124

Earlier quoted context omitted.

Forgive the authors of the article for assuming readers would complete it.

For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side. Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?

Isn’t deciding what responsibilities there are in any text very much in the author’s side and not yours?

Haven’t you dramatically overstated your case? Many expositions do not contain an explanation of their value at all. Works of fiction are a good example, and there are many many others. Often it’s the responsibility of the readers & reviewers to decide on questions like value.

Re: Formalizing Fermat's Last Theorem

#444

Post by YeGoblynQueenne »

SkidanovAlex wrote: post #369
gorgolo wrote: post #367

Earlier quoted context omitted.

> That theorem statement is correctly encoded (FLT has a very short 1 liner description really) As someone not very familiar with Lean, does it really just depend on the entry point / theorem being correctly encoded? Can intermediate statements ever be mis encoded or misinterpreted, or is this what would count as a “bug in the Lean compiler”?

It is the latter. If you are certain your theorem is stated correctly, and you believe that the Lean kernel against which you validate is correct, your proof is correct. This is how the theorem for FLT looks in the particular proof we discuss here: theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of…

Couldn't the kernels have different bugs?

Re: Formalizing Fermat's Last Theorem

#445

Post by contubernio »

glimshe wrote: post #205

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…

As a mathematician not expert kn these things, yes it scans as reasonable, and yes it has me and most of my colleagues reconsidering what we do for a living.

Re: Formalizing Fermat's Last Theorem

#446

Post by fspeech »

fspeech wrote: post #385
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.

To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.

The webpages are entirely generated without a binary build (a build from scratch is quite daunting as stated in the project readme) of Lean artifacts. See https://github.com/anthropics/fermats-last-theorem/blob/main...

Re: Formalizing Fermat's Last Theorem

#447

Post by YeGoblynQueenne »

voidhorse wrote: post #424
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…

To me, a lot of the child comments on this thread are technically correct (the best kind) in that, yes correctness bugs in Lean boil down to compiler bugs in a language like lean. What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode is still a major problem and yes, extremely difficult when you have that many lines to pore over. But, if you're using LLMs t…

No expertise at all on interactive theorem provers like Lean but I am familiar with Resolution-based automated theorem proving. In that setting, one writes down a theory, in the form of a set of first-order definite program clauses, and then presents a statement to the prover, then the prover proceeds to prove the statement is a theorem derived from the theory.

Is that (other than the language not being definite logic) more or less what Lean does also? In that case, isn't all the work in writing down the theory, and isn't that the step where mistakes can creep in?

Is that more or less what you're pointing out? That FLT is simple enough to state but the theory from which it is to be derived can be mangled and so accept FLT on the wrong grounds?

Re: Formalizing Fermat's Last Theorem

#448

Post by YeGoblynQueenne »

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.

It doesn't seem execution was a problem. From Kevin Buzzard's blog:

I’ve compiled the code base and run comparator on it — it checks out. It is a gigantic proof (over 13.4 million lines of code) and takes nearly 20 times as long to compile as Lean’s mathematics library (on a machine with 96 cores!). Lean can be sluggish when jumping from file to file on a repo of this size (even on a machine with 500G of ram, which Anthropic also gave me access to), but Anthropic also supplied me with some html documents which are easier in practice to explore (clone the repo and open with a web browser).

500G of RAM is not actually that huge tbh (I was looking to buy a used 1TB server blade for some personal stuff a while ago but it was too much hassle) so I don't guess there was too much potential for buffer overflows.

Re: Formalizing Fermat's Last Theorem

#449

Post by contubernio »

floweronthehill wrote: post #129
ojo-rojo wrote: post #95

I'm really impressed by mathematicians. It's cool that Fermat had the intuition to conjecture that "aⁿ + bⁿ = cⁿ" could not be satisfied for n > 2, and that other mathematicians can create proofs, and that others still can understand AI's formulation of those proofs. Really cool.

I wonder if AI can come up with mathematical conjectures. As in, they feel it's right but can't prove it. What even happened in Fermat's brain to sense it was true?

It is capable of applying know heuristics and general principles in places where they haven't been applied and in this sense very much capable of generating conjectures in much the same way a person does. It's ability to employ a diversity of techniques coupled with it's computational power differentiate it from a human researcher. It still needs guidance to work well, but I've already changed my daily work flow as a research mathematician to incorporate use of AI.

Re: Formalizing Fermat's Last Theorem

#450

Post by YeGoblynQueenne »

contubernio wrote: post #445
glimshe wrote: post #205

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…

As a mathematician not expert kn these things, yes it scans as reasonable, and yes it has me and most of my colleagues reconsidering what we do for a living.

Well, if I were a mathematician, what I'd be noodling about with right now is a way to model the number of failed attempts that AI companies must be making for every success they report.

I guess you don't have to be a mathematician to do that sort of calculation, but I'm just proposing it as a way to lift mathematicians' spirits a bit.

Also pay attention to the fact that every time a new model is released there's a slew of new results and then they dry out for a while, which suggests a "throw stuff at the wall and keep what sticks" approach that's incompatible with a kind of system that can just magickally solve all maths right now.

I'm saying that because I get the feeling that mathematicians don't have a good model for the true capabilities of those systems and that can lead to an overreaction, like "woe is me, all of mathematics will be solved and my entire discipline will be rendered obsolete". Coming from an AI background I don't think that's right. I think because mathematicians are not AI researchers they simply don't have a very clear idea of what's going on with those systems. And tbf even many AI researchers (the ones who don't enjoy the benefits of a long tradition that goes back to the 1950's and basically only joined the field in the last 10 years or so) don't understand those systems very well either.

Bottom line: don't panic.

Or, not yet :0)

Post reply on HN