Live data from Hacker News

Formalizing Fermat's Last Theorem

anthropic.com

381–390 of 527 posts

Re: Formalizing Fermat's Last Theorem

#381

amazing, it's a huge achievement. can someone clarify, where the writeup says "The finished proof was checked by Lean; it uses just Lean’s three standard axioms" what does this mean? Aren't there a large set of standard axioms that are also necessary? (i.e. ZFC+)? if not, since it's only three axioms, can someone say what they were?

I don't really know Lean, but I think this means, three axioms on top of their whole type theory machinery, to make it classical. The type theory machinery is the obfuscated encoding of the large set of standard axioms that they don't tell you about. For example, they can encode natural numbers using that machinery.

Re: Formalizing Fermat's Last Theorem

#382
post #377

Earlier quoted context omitted.

A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.

Wouldn’t a lot already be in leans mathlib?

AI is hopeless at using existing code, it likes to append only.

Re: Formalizing Fermat's Last Theorem

#383

Earlier quoted context omitted.

But US also spends too much on education as well. The issue doesn't seem to be funding but the educational reform like in mississippi, where they increased student performance without increasing their budget too much. That's why you see bad k12 educational outcomes compared to the budget spent in blue states. It's all about efficiency. Give AIa chance in few years as I feel it can make great strides.. it's hard to im…

You see funding of chatgpt as a panacea for progress. I see funding of chatgpt as one of small part of a history where governments and industry fund basic science and moonshot programs, not to generate revenue, but to explore what is possible. LLM funding is not aimed at improving our understanding of the world, it's aimed at making people reliant so that they may extract wealth through subscriptions for shareholders…

Why can't it both? Of course they are not gonna do it just because it improves the world and understanding but because there's an incentive to align money with progress. Even the vaccines initially were distributed to get monetary gains and as the government started subsiding it as well, it became cheaper to produce.. that's basic capitalism and markets and regulations 101, no human is that selfless to give it out for free and they shouldn't because it's their investment in time, money, effort etc. but we should strive to align the greed aspects with good outcomes.

No Americans get fat and don't have a personal responsibility to maintain their health.. no amount of free healthcare is gonna change that.. they vote for free healthcare, see their taxes raise, then vote against cz they don't see tradeoffs in life.. it's better to maintain better habits than rely on govt to subsidize bad behaviour. There should be some basic coverage for poor people but not too much to sustain irresponsibly

Re: Formalizing Fermat's Last Theorem

#384
post #14
post #4

Wow -- looks like thanks to Claude, Lean checks off another box on https://www.cs.ru.nl/~freek/100/

The last box, per https://news.ycombinator.com/item?id=49568667

Has Lean proved the Four Colour Theorem? I thought only Rocq had.

Re: Formalizing Fermat's Last Theorem

#385

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.

Re: Formalizing Fermat's Last Theorem

#386
post #6

An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable. I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think…

There are a couple of proof languages that are designed for formalized mathematics (rather than formal verification of software) and to be readable by mathematicians. For example, look at the proof that square root of 2 is not rational written in Naproche (retyped from [1], typos are mine):

Theorem. $\sqrt{2}$ is irrational.

Proof.

Assume that $\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction.

Qed.

Or, say Isar in Isabelle/ZF [2].

There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are.

[1] https://ceur-ws.org/Vol-448/paper10.pdf

[2] https://isarmathlib.org/UniformSpace_ZF_1.html

[3] https://mathoverflow.net/questions/513742/are-we-stuck-with-...

Re: Formalizing Fermat's Last Theorem

#387

Earlier quoted context omitted.

I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.

It seems unlikely to find 1920 level or so proof although it might be the case that a significantly easier/shorter proof exits via Vandiver conjecture + extra work or Effective Mordell conjecture but it also wouldn't surprise me if that would be even more complicated than the current proof of FLT.

Yeah Vandiver was on my mind, this is why I said 1920. Wouldnt mind it more complicated, but with simpler concepts and most importantly concepts that feel like they have something to do with FLT (cyclotomic fields, not modular forms).

Re: Formalizing Fermat's Last Theorem

#388

Earlier quoted context omitted.

Which metrics are poisoned? Can you provide your arguments for why Good heart's law applies here and how and which metrics are bad measures? For b, can the writer at least provide their own thoughts or are they gonna leave it as exercise for some others to fill in?

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 able to improve their catching skills with lesser cost or they have more funding or there is more demand for fish..all of these help their company grow as they have to balance out cost/benefits like any business should. If the company is currently in loss but still lives on, it's cause either govt subsidizes it or they're expecting future profit so they can temporarily bear out the costs like amazon did and jz grow as company with capital and all.. you are actually not aware of wealth of nations or any basic economics book? There are gonna be tradeoffs with more wealth and externalities but on net, they seem better than not having wealth, gdp etc..

Human dignity lol.. when have that ever been the case that we respected human dignity? We had communist and fascist regimes commit atrocities like there's nothing and we're still too cowardly to fight the Iran or russian regime to liberate their citizenry from their dictatorships. Please don't make me laugh by saying that AI decreases human dignity when we never respected it in the first place. With AI and markets and liberalism, we can finally free citizens from tedious work and focus on important work like innovation.

1. Am I reading fiction or what? Companies can only sustain themselves if broad members of society can pay to it.. that's why even right now, AI companies are struggling to be profitable where only very few people are paying for it and cz many people are not even aware of the progress and capabilities of AI in different fields. You can easily use local LLMs which are only 6-12 months behind in frontier models if you are so anti business. The benefits still can be utilised by an amateur in their own PC. Of course, they will try to restrict others from distilling as they want to be monopoly but what we want to do is make them be productive to society as well by providing their services for cheap which they're doing. Your screed just feels more like fantasy than real world economics.

2.oh my lord, what kinda idiocy is this? U can free/local models and run in local for dirt cheap and still have epistemic wealth to yourself if you are so worried about it. None of your arguments permit human agency at all.. I'm conscious that anthropic wants me as reliable costumer so that they profit from it but I would pay only if it solves my problem. Whenever I pay, I know that they can terminate if they want but I'm not just restricted to their models. You don't have arguments, you have stories/ted talks.

Re: Formalizing Fermat's Last Theorem

#389
post #268

Earlier quoted context omitted.

Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat

I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.

Of course, there's a possibility but it exists everywhere but there's no sign till now that it has. Same with openai's proofs.

Re: Formalizing Fermat's Last Theorem

#390
post #327

Earlier quoted context omitted.

Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat

How about all of these bugs from last week? https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t... ...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".

Sure. But experts seem to be aware of the direction of those solutions so it seems unlikely there could be some hidden bug which disproves it. But it could be possible.
Post reply on HN