11 ms·
Formalizing Fermat's Last Theorem
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
- richard_chase 14d agoAnyone know of a good Lean tutorial? I've played around with it a bit but never really learned it properly.
- deleted 14d ago[deleted]
- throw567643u8 14d agoI'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.
- Jblx2 14d agoNot mm0?
- kdavis 14d agoImpressive! Buzzard's group[1] got scooped. [1] https://github.com/ImperialCollegeLondon/FLT https://github.com/ImperialCollegeLondon/FLT
- arjie 14d agoSeems to have taken it in good spirit: > We shared the resulting proof with Kevin Buzzard, who said: > > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.
- ajs1998 14d ago> What this work is, and is not > I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway). > Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK, and most people in the number theory community are 100% sure (formalization has made me more paranoid about the mathematical literature than most). From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
- lalitmaganti 14d agoI suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment, what it means but also doesn't mean.
- BeetleB 14d ago"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…" Gives you an idea of the scale...
- sebzim4500 14d agoIt sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.
- _aavaa_ 14d agoUnlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
- alch- 14d agoI don't think Anthropic is turning a profit ;)
- dist-epoch 14d agoNeither did Amazon for it's first 25 years ;)
- caughtinthought 14d agoI think you're missing the point of the comment you responded to, lol.
- andrewla 14d agoWow -- looks like thanks to Claude, Lean checks off another box on https://www.cs.ru.nl/~freek/100/ https://www.cs.ru.nl/~freek/100/
- rawling 14d agoThe last box, per https://news.ycombinator.com/item?id=49568667 https://news.ycombinator.com/item?id=49568667
- throw567643u8 14d agoHas Lean proved the Four Colour Theorem? I thought only Rocq had.
- Smaug123 13d agoIt’s an aggregated list, not a list of formalisations in Lean - the checkbox is “things formalised in any prover”.
- deleted 14d ago[deleted]
- kristjansson 14d agoWell, time to set down the glass beads and dive into a an alpine lake.
- alberto-m 14d agoThere are hopefully still some Ludi to play before doing that, Magister.
- vetronauta 13d agoCurrently a tiny fraction of what is formalizable is of interest to mathematics; maybe humans will stop doing "serious" mathematics, but mathematics is beautiful and we will not stop playing with math, like we did not stop playing chess. I would love to see a theory in the spirit of Guerino Mazzola work, but for (combinatorial) games.
- rao-v 14d agoAn 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 about proofs. My very brief attempts at Isabelle / RCoq feel more natural. I think it's a pity that the future of proofs is Lean. I'd love for someone to come up with a more digestable proof language!
- gowld 14d agoThat's like saying the future of code is Assembler. Lean is not for humans.
- epgui 14d agoLean is for humans.
- SirHackalot 14d agoInteresting to find this comment, I’ve been dipping my toes into formal methods and was doing a RCoq tutorial yesterday (really basic stuff), and I also noticed that the proofs in RCoq have a more pen -and-paper proof feel to them.
- rao-v 14d agoRight? Might be worth another shot
- c7b 14d agoIf you're doing it for fun anyway, why not use the language that gives you the most pleasure?
- voxl 14d agoHearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.
- m_w_ 14d ago> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.
- jameshart 14d agoThere is no way Fermat could have fit that in the margin. Definitely vindicated.
- bananaflag 14d agoI am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.
- HappyPanacea 14d agoIt 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.
- bananaflag 14d agoYeah 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).
- arjie 13d agoI read an interesting take that it won’t. Because it won’t be interesting any more. It’s like how no one talks about AI IMO Gold anymore or Stockfish being better than all humans. This kind of mathematics goes back to being a curiosity of humans and machines move to the next frontier. In a sense, the proof is a demonstrator not an end in itself. To mathematics enthusiasts it is significant. To the AI it is Tuesday. Enjoyed that idea. Not sure how true but it was enjoyable.
- baq 14d ago[flagged]
- baggy_trough 14d agoStochastic parrot truthers in shambles.
- Vakaiser 14d agoWe'll increasingly observe announcements of this kind as AI tooling scales. As impressive as agentic coding is, it pales in comparison to the value proposition of medical, mathematical, and physics research. I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts. Cost effective large scale genetic engineering, a cure for every disease, potentially even a cure for aging. The future is both beautiful and terrifying.
- rowanG077 14d agoI dont think it will happen. AI models are kneecapped. Only a tiny tiny tiny fraction of people are on the list of even being able to use these tools for such things.
- sebzim4500 14d agoEven in a world where these models are heavily restricted, surely the likes of cancer researchers will be among those who have access
- tinfoilhatter 14d agoIt's wild to think that aging is something that needs to be cured, and isn't a part of the natural human experience. I'm so tired of people trying to play the role of God, as well as people that cheer these sorts of things on.
- sebzim4500 14d agoI hope you keep these horrible thoughts to yourself if you ever walk through a paediatric hospital
- tinfoilhatter 14d agoThinking that aging is a natural part of the human experience is a horrible thought? Please explain...
- lseplot 14d agohttps://github.com/anthropics/fermats-last-theorem/blob/main/formalization.yaml https://github.com/anthropics/fermats-last-theorem/blob/main... status: "self-assessed" 13 million lines of Lean, where the Lean and Nanoda kernels missed the Collatz hack. Fable, please translate to HOL-light. Make no mistakes. You are doing great!
- voxl 14d agoIt's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another modest increase in trust, but to pretend the implementation of HOL-light has never had bugs and it's kernel could never have a bug is hubris.
- 3192987 14d agoWe have a significant case split here: A human mathematician writes a Lean proof: - Unlikely that the mathematician would cheat with Lean bugs or even know how to find one. Trust increases. An AI writes a Lean proof: - AIs have been "ambitious" in their goals in the past and do know how to find Lean bugs and exploit them. Trust decreases.
- aaraujo002 14d agoThey released the code here: https://github.com/anthropics/fermats-last-theorem https://github.com/anthropics/fermats-last-theorem
- sigmar 14d ago>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work. ^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
- t_gamer_kle 14d agoForgive the authors of the article for assuming readers would complete it.
- finjo 8d agoHave you written text for humans? You’re lucky if you can get people to read more than the title. You’re very lucky if they read past the first paragraph.
- salomonk_mur 14d agoFor 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?
- HappyPanacea 14d agoBuzzard is writing for his blog audience - mostly mathematicians and not the casual visiting HN user.
- jibal 14d agoEh? The quote is from Anthropic, not Buzzard.
- beepbooptheory 14d agoFeel very grateful I was never taught this... Would have missed out on quite a lot of good bodies of text in my life I think! Pushing through any initial friction or ignorance I might have as a reader, having the patience and charity to bear with an author until you get it, was instead what I was always taught. Giving such a blanket "responsibility" to the author at all is just such a bummer! I say let them do whatever they want, there is always more than one way to express oneself. Someone who was never taught to write a clear thesis in the first paragraph for whatever reason doesn't inherently have less to say.
- baggy_trough 14d agoI won't be impressed until it identifies the proof he wrote in the margin. /s
- jrflo 14d agoHoly shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?
- bjourne 14d agoYep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.
- simpaticoder 14d agoBut isn't that understanding discarded? It is if you mean "intermediate working state" while it was generating the LEAN code. Which raises the question: I wonder what other directions it could have gone in those intermediate states? Is it possible to snapshot the state of an LLM (or a cluster of them) "in the middle of proving FLT" and then prompt it to go in a different direction with all that context?
- bigstrat2003 14d ago> Now we add an LLM to that list. No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.
- bjourne 14d agoA meme free of charge for you, sir: https://www.reddit.com/r/singularity/comments/1jl5qfs/its_just_predicting_tokens_v2/ https://www.reddit.com/r/singularity/comments/1jl5qfs/its_ju...
- traes 14d ago25-50 seems like a pretty lowball estimate, I guess depending on your definition of "understand."
- mswphd 14d agonot really. it's one of the most difficult ones so far for sure, but pales in comparison to something like the classification of finite simple groups. This was initially "completed" in the 80s. You can see the timeline for cleaning up the proof in e.g. this mathoverflow answer https://mathoverflow.net/questions/114943/where-are-the-second-and-third-generation-proofs-of-the-classification-of-fin/217397#217397 https://mathoverflow.net/questions/114943/where-are-the-seco... it's something that some people have been waiting decades for, and is not yet completed.
- atleastoptimal 14d agoIt seems clear AI has the potential to perform any cognitive task at far greater speeds, reliability, and scale than any human. The question is whether it will be allowed to scale to that point, and what will happen to humans after this occurs.
- dakolli 14d agoYou'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead. Not sure why anyone is excited about this tech.
- artifact_44 14d ago[dead]
- yesitcan 14d agoSo much doom and gloom on this site. Makes it almost not worth reading.
- justonepost2 14d agomaybe that's because the doom and gloom is the transparently correct outcome?
- CaptWorld 14d agoWhy? Even communists weren't this doomed and were actively rooting for it to solve the economic calculation problem which ai might take us to. People are just pessimistic in general ig
- justonepost2 13d agohttps://borretti.me/article/no-one-escapes-the-permanent-underclass https://borretti.me/article/no-one-escapes-the-permanent-und... This is probably the best and succinct explanation of what’s coming.
- somberi 14d agoOn a tangential note, I highly recommend this book by Simon Singh. https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book) https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)
- raverbashing 14d ago100% It is a very insightful book
- The_Blade 14d agoi read it from a library. this all just makes me feel cozy and nostalgic and uplifted and sad all at once
- dominotw 14d agoone of the most popular books in india growing up. used to see it everywhere
- OroPla 14d agoMakes me feel old again. I read this over twenty years ago.
- wrboyce 11d ago“The Code Book” and “The Simpsons and Their Mathematical Secrets” are also great books by the same author.
- bluecalm 14d agoVery impressive! I was a child when that proof came out. I've read a book about it a few years later and used it on my final high school exam. I remember some friends trying to understand parts of it at univ. It was all like black magic to me and the vibe was "maybe a few people in the world understand it". I hope soon enough we will have one of the big ones proved by AI!
- dakolli 14d ago[flagged]
- anony-123 14d agoSo, what I am thinking is that, the AI generated numbers or tried to find numbers "a", "b" and "c" to check if aⁿ + bⁿ = cⁿ Can not we do it by code?
- sweetheart 14d agoLean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.
- yesitcan 14d agoIf they’re asking that kind of question, do you think this answer will help them understand anything?
- sweetheart 14d agomaybe it will be an answer that entices them to understand more :)
- kzrdude 14d agoYes
- estetlinus 14d agoSure, go on and try it ;)
- charlieyu1 14d agoI found a brilliant proof but there was not enough hard disk space to save the file :(
- kbelder 14d agoJust loop through all values of a, b, c, and n?
- drivebyhooting 14d agoLLMs are pretty good at slogging through. When will they come up with brilliant breakthroughs like Andrew Wiles?
- chpatrick 14d agoAbout two month ago: https://en.wikipedia.org/wiki/Jacobian_conjecture https://en.wikipedia.org/wiki/Jacobian_conjecture
- thrance 14d agoCome on, you can't compare that with Wiles's proof.
- drivebyhooting 14d agoThat’s just a counter example I can check by hand with almost zero background. Wiles’s proof will remain a mystery to me.
- traes 14d agoWe have absolutely no idea if this was a brilliant breakthrough or not. They haven't released any explanation of how it was found. A problem being old and prestigious does not mean its solution is automatically a brilliant breakthrough.
- estetlinus 14d agoI can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It’s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.
- aidos 14d agoAlso recommend his other books! Big Bang - history of the understanding of space and the universe Code book - history of the maths of ciphers Haven’t read them for years but I’ve been meaning to again
- FergusArgyll 14d agoOoh I never realized FLT and Code book were the same author. Yes, both great!
- kzrdude 14d agoAnd the multiple Numberphile appearances of Ken Ribet are interesting too! He is incredibly well spoken. - https://www.youtube.com/watch?v=nUN4NDVIfVI https://www.youtube.com/watch?v=nUN4NDVIfVI (The bridges to Fermat's Last Theorem) - https://www.youtube.com/watch?v=NPOw4iIxN6o https://www.youtube.com/watch?v=NPOw4iIxN6o (podcast)
- KaiserPister 14d ago13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?
- tossandthrow 14d agoThe proof system is relatively easy to verify. I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code. You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.
- Jaxan 14d agoMost systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)
- tossandthrow 14d agoYou need to understand the concept of the core algebra and 100s (with the s), then I think you'd be better positioned to understand my comment. And granted, I don't know the exact details about Lean. It might be that they don't have an incredibly simple core - as has elsewise been the norm.
- Jblx2 14d agothe Nanoda type-checker for Lean is ~5,000 lines of Rust: https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/ https://leodemoura.github.io/blog/2026-3-16-who-watches-the-... ...and for those who are looking to roll-their-own: https://ammkrn.github.io/type_checking_in_lean4/title_page.html https://ammkrn.github.io/type_checking_in_lean4/title_page.h... ...and some thoughts on putting stuff in the kernel: https://lawrencecpaulson.github.io/2026/07/30/Collatz.html https://lawrencecpaulson.github.io/2026/07/30/Collatz.html
- holmesworcester 14d agoNope! :( Meaning, people and LLMs are finding 1=0 bugs in formal verification tools. I have no idea how likely this is in this case, though!
- kzrdude 14d agoThe 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?
- simpaticoder 14d agoThis stuck out to me, too. That a (presumably rather simple) coworking tool was instrumental in shaping the vast (6B token!) output is eye-opening. We have this vast power but without intermediate structure it is wasted. Much like Turing machines themselves, which are shaped by language design to get somewhere at the expense of getting everywhere.
- marwahaha 14d agoI helped build https://prove2.me 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.
- refibrillator 14d agoProving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye: https://news.ycombinator.com/item?id=49203626 https://news.ycombinator.com/item?id=49203626 It is truly saddening to think that machines will deprive us of this wonder and experience. But truly exciting to dream about what lies beyond the limits of our biology.
- bawolff 14d agoFormalizing is not the same as discovering. There is still plenty of room for human ingenuity.
- mannanj 14d agoMakes me wonder, if we make a tradeoff for comfort and advancement from our biology's "limits" - and that tradeoff is spiritual fulfillment. Seeing it hit across: the work we used to do outdoors, the sleep-wake-dark cycle we adhered to for millennia, and more
- ben_w 14d ago> It is truly saddening to think that machines will deprive us of this wonder and experience. It won't deprive us. Recent video I've watched from Brandon Sanderson, IMO also applies to all the things we love and not just art: https://youtu.be/mb3uK-_QkOo?si=SG1uvGUbN6SOYI_J https://youtu.be/mb3uK-_QkOo?si=SG1uvGUbN6SOYI_J
- stabbles 14d agoNow /simplify. Can it be half the size? Will someone at some point prove that the proof cannot be simplified further?
- raverbashing 14d agoYes. FLT follows from the fact that you can't build the equivalent representation of n-simplex turning into a hypercube in dimensions higher than 2 /s
- prometheus1992 14d agoCan someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?
- hyperhello 14d agoThe 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.
- epgui 14d agoIs Lean a DSL? I’d argue it’s a general purpose programming language that excels at proofs.
- hyperhello 14d agoWell, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
- mswphd 14d agoit is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.
- stratos123 14d agoencode 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 https://github.com/James-Hanson/junk-theorems-in-lean
- hyperhello 14d ago
- ex-aws-dude 14d agoTo ask a dumb question is there any chance there can be a bug in these generated proofs that makes it think its true? Or is it the case that as long as you verify the initial statements you are trying to prove the rest doesn't matter
- QuesnayJr 14d agoLean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).
- forkbomb123 14d agoI'm so curious what happens to this project that intended on proving FLT by 2029 now the project: https://imperialcollegelondon.github.io/FLT/ https://imperialcollegelondon.github.io/FLT/
- hokkos 14d agotheir reaction here : https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
- dgellow 14d agoLean continues to pay off. Such a beautiful project
- davmre 14d ago> a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1. At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.
- 3192987 14d agoAnd human salaries for those who worked on the prover harness etc. which isn't just standard Fable. It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged. Now they have it in writing.
- logicprog 14d ago> A fact that LLM hawks have categorically denied here before, with opposition naturally flagged. Yeah, because before now there's been literally zero proof of an automated theorem prover scaffold around the LLMs being used, and big counterexamples and such being found, with raw chat logs available, where no such thing was used. > Now they have it in writing. Yeah, because now it's actually being done. They talk about it as a novel thing, because it is. You don't get to claim being "right all along" from this
- 123aHgf 14d agoWrong. AlphaProof is much older, used Lean and a tree search for tactics just like ACL2. They all steal from ACL2 without attribution in the current publication boiler room atmosphere. They get away with it because the AI Cult has information and publication dominance. There was a brief period that used only language for toy IMO problems, but for serious work like FLT they apparently reverted to established approaches.
- porridgeraisin 13d agoLiterally many previous instance used one. Right from alphaevolve onwards. I'm not some "LLM is just a next token predictor guy" (GP seems to have a thing against LLMs), but to use LLMs properly you genuinely do need a grounded verifier and a planner. Coding harnesses for example are exactly that. For some plans, you can AR generate the search tree and that's what subagents being planned around by high level (LLM)agents and such are. Coding agents even with subagents are imperfect even on verifiable tasks only because of that. If you can put a human to simply guide it, it becomes a full system. This is what we all do today whenever we use codex. It's not something that is "never done before". I also don't subscribe to the purist view which is taken by GP. I prefer to think in terms of concentration inequalities. P(failure rate > r) < epsilon. You get different levels of autonomy for different values of r for the planner and verifier each. If you have a good planner and a good verifier, r is very very small and it's super useful. Autonomy at a given r comes from how much of the planner and how much of the verifier is automated at that r. All levels of autonomy are economically useful. Many values of r are economically useful. In this case of FLT, the verification was entirely automated using lean, and it is correct upto lean compiler bugs (so a very small r). The planner was essentially a maintained graph (afaik. Prove2me doesn't use A* or any heuristic/evolutionary methods to limit or prune the frontier), AND importantly - I'm not seeing anyone on HN mention this - some human nudges, literally, which nodes to open. The way to make AI systems more useful is to build great verifiers and great planners, which is what many companies and startups are doing. LLMs are already really really good proposers due to excellent generalization (to be pedantic, multiple stacked specialisations), especially MoE models, making them amenable to proposing at every point in a vast search tree without any adaptation. Yes, it is possible to do complex tasks purely AR, so long as you can AR simulate the search, which in the case of LLMs corresponds to verbalising the search tree[4]. This is trivially true. Can this be useful? Yes. Can a millenium prize problem be solved purely AR? Sure. It's a hard problem for humans, there is no reason it has to be difficult to reach in the conditional distributions of every future LLM. In the trivial limit, an LLM trained on the solution 100% you can sample it out. An LLM 2 generations behind that may have it at p=0.001, entirely reachable given a planner, but probably not AR. An LLM 1 generation behind may have it at p=0.05, plausibly reachable purely AR. But the key question is: is `r` smaller or larger if you have a planner versus not? The answer there is obvious. Second, if you have a threshold `r` that decides usefulness, is the set of things you can autonomously do under that threshold higher with planners and verifiers? Again the answer is an obvious yes. Copy pasting code from chatgpt repeatedly is worse than using a coding harness where it gets grounded feedback, LLM weights kept constant. Keeping the history of things and the overall plan that worked fixed and isolating LLMs to do subtasks is better than developing a whole database in one continuous context. In some cases, the overall plan "tree" can itself be entirely verbalised, but most commonly there is human modifications/steering. Can pure-LLM coding harnesses with just verifiers one shot most e commerce sites including planning? Yes. But we want to do more with it than e commerce sites. Will it keep improving thus enabling us to do more and more complex things? No obvious reason for a fixed limit to exist in theory[1]. But at any point on the progress curve, using it with a harness always gives better results versus not. Concretely, with fable 5.1, using it without a harness could not prove FLT in reasonable token budgets [3]. However, it is possible for say, idk, GPT9, trained on this, to verbalise this whole proof tree, and also potentially generalize it to another open problem, purely AR, in a reasonable token budget[2]. This was how we got from gsm8k to FLT in the first place. It's not a binary "AR is useless" "AR is all you need". [1] the limits are mostly economic, and time is itself a limit, see https://news.ycombinator.com/item?id=49161078 https://news.ycombinator.com/item?id=49161078 Tl;dr diminishing returns of test time scaling. Noam brown also has a piece about this. [2] if it's too many tokens that we run out of time or money literally, that is the limit described in [1]. It is not linear or constant scaling necessarily as described again in [1]. [3] [2] is why we have to add token budgets as another axis apart from r and the autonomy level. [4] And, the distribution conditioned on that verbalisation must be amenable to sampling the verbalisation of the execution of the plan from. This is not a given, see https://arxiv.org/abs/2504.09762 https://arxiv.org/abs/2504.09762 and https://news.ycombinator.com/item?id=49277303 https://news.ycombinator.com/item?id=49277303
- mhmdfromkarak 14d agothat's crazy
- deleted 14d ago[deleted]
- chvid 14d agoLooking forward to the 5 billion LoC proof of the Riemann hypothesis.
- alok-g 14d agoIf AI manages to prove, or disprove, I wonder what would Clay Foundation do for the prize.
- deleted 14d ago[deleted]
- ReptileMan 14d agoWhy didn't you ran them to find simpler proof? This could also be big.
- fn-mote 14d agoThat's next week's work.
- ojo-rojo 14d agoI'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.
- floweronthehill 14d agoI 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?
- ojo-rojo 14d agoRight. Once we see AI start delivering on the creative & intuition side of things that's going to be awesome. Until then I guess we'll live with exhaustive exploration of problem spaces by orchestrating swarms of agents...?
- contubernio 14d agoIt 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.
- henryrobbins00 14d agoBack in February, I was talking with my PhD advisor about using Lean to formally verify automated optimization modeling outputs. It eventually turned into this paper [1]. It’s been truly incredible to see how much the frontier models have progressed in both autoformalization and automated theorem proving in the last six months. Back in February, it was cool to see them prove the validity of some simple cutting planes. Now it can churn out a min-cut max-flow duality formalization (not to mention FLT). Very exciting times! I’ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2]. [1] https://arxiv.org/abs/2608.25220 https://arxiv.org/abs/2608.25220 [2] https://github.com/henryrobbins/open-atp https://github.com/henryrobbins/open-atp
- fspeech 14d agoFirst I have to say this is sooner than expected, even though I never doubted that this could be done. I am grateful that they dedicated resources to accomplish this. It is clear that agents are very good at discerning and holding onto very weak signals from RL traing on long horizon tasks, so much so that in my own experience even very chaotic agent thinking can converge to meaningful solutions if there is a verifier. I have not dug through the proof yet so I don't know how readable it is to a human. But it has been a dream of mine to understand the FLT proof. I think LLMs will be a big part of making it truly accessible to humans.
- chi_features 14d agoThere's a wonderful documentary by BBC Horizon with Andrew Wiles from 1996 – highly recommend! I saw it in the 90's and it's a documentary for everyone. It captures the effort, struggle, highs and lows of a 7 year effort working on Fermat's Last Theorem.
- martinpw 14d agoLooks like it is available here: https://www.dailymotion.com/video/x3wrbsb https://www.dailymotion.com/video/x3wrbsb
- AmazingEveryDay 14d agoAlso: https://archive.org/details/BBCHorizonCollection512Episodes/BBC+Horizon+-+s1996e02+-+Fermat's+Last+Theorum.avi https://archive.org/details/BBCHorizonCollection512Episodes/...
- tonyedgecombe 14d agoAlso https://www.bbc.co.uk/iplayer/episode/b0074rxx/horizon-19951996-fermats-last-theorem https://www.bbc.co.uk/iplayer/episode/b0074rxx/horizon-19951... (if you are in the UK).
- deleted 14d ago[deleted]
- catigula 14d agoAn AI safety company!
- enriquto 14d agobut i don't understand... isn't Wiles's proof and its numerous rewritings already in the training set?
- QuesnayJr 14d agoOf course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.
- tatjam 14d agoI think there's a big misunderstanding going on here, translating the proof to Lean is, well... a translation task. Formalizing the proof in a way that's useful (breaks the proof down into relatively independent blocks that can be used for other maths and, importantly, understood individually) is a quite bigger, more creative endeavor. Not sure if LLMs would be able to do it, maybe yes?
- mswphd 14d agonote that this is exactly analogous to an LLM being able to slop code some demo, but not build something more generally useful/maintainable (say something suitable for inclusion in a standard library).
- QuesnayJr 14d agoIt wasn't clear that LLMs were up to a Lean translation task of this scale until now. The background required to formalize the FLT proof was tremendous, so many people assumed we would have to wait until all of that was formalized in Lean before we could ask it to formalize Wiles' proof. Now it seems like almost any mathematics paper we can ask an LLM to formalize, including all necessary background, and it can just do it.
- deleted 14d ago[deleted]
- 14d ago
- crawshaw 14d agoMore (strong) evidence that agents make formal methods far more useful. The cost of creating that Lean proof has dropped dramatically. Hopefully this helps mathematicians. It seems very clear to me that it will help software engineers apply formal methods to more of our software.
- QuesnayJr 14d agoHoly shit. The proof of FLT is a giant detour through several different areas of mathematics, so formalizing it is a lot of work. An interesting next target would be formalizing the classification of finite simple groups. The original proof scattered over thousands of pages of journal articles, plus Aschbacher and Smith's 1300 page 2 volume monograph. It's so long it's hard to know if there are any gaps. Researchers have been working on a streamlined new proof, but it's already many volumes long.
- sanxiyn 14d agoNew proof: The Classification of the Finite Simple Groups (American Mathematical Society Mathematical Surveys and Monographs vol. 40). https://www.ams.org/publications/authors/books/postpub/surv-40 https://www.ams.org/publications/authors/books/postpub/surv-... Number 1 (1994), Number 2 (1995), Number 3 (1997), Number 4 (1999), Number 5 (2002), Number 6 (2004), Number 7 (2018), Number 8 (2018), Number 9 (2021), Number 10 (2023). 10 volumes and >4000 pages so far, number 11 is in progress, and end is in sight, probably two more volumes or so. https://www.ams.org/journals/notices/201806/rnoti-p646.pdf https://www.ams.org/journals/notices/201806/rnoti-p646.pdf People were curious what is going on during 2004-2018. A progress report was published in 2018 right before publication of number 7 and 8. In a sense it was the peak, number 8 completes the proof of so-called "generic case". The rest is "special case". It doesn't mean things get easier, but in some specific sense number 8 completed proof for almost all groups. Now new proof's end is in sight, people are planning new new proof.
- victor22 14d agoI call bullshit on 13 million lines makes no sense
- deleted 14d ago[deleted]
- traes 14d agoThe repo is public. You can just go look! It's really not that surprising; FLT is huge and has a ton of dependencies that need to be implemented, and there's a degree of sloppification that is probably blowing up the size by a few factors.
- vatsachak 14d agoThis is quite useless actually. The whole point of formalizing FLT was to clean up modern number theory into reusable abstractions that prove it. If its 13 million LoC, it might involve so much spaghetti that its unusable other than the result
- The_Blade 14d agophysics is like sex: sure, it may give some practical results, but that's not why we do it
- vatsachak 14d agoI mean at this point there's no doubt that LLM cans be RL maxxed and give you _some working output_ but the next frontier is whether they can create good abstractions, a.k.a use the correct level of expressivity so as to not inline everything yet not play code golf.
- whateveracct 14d agomy feel after a lot of experience with agentic haskell at scale has been...no they cannot and maybe the opposite lol
- vagab0nd 14d ago> it wrote 13 million lines of Lean Is this basically like opening up a black box and seeing 13 million gears all rotating seemingly randomly and still having no idea how the machine actually works?
- qbane 14d agoThat is already the case for most neural networks and LLMs.
- JacobAsmuth 14d agoExcept there's 10 trillion gears
- saadyousfi 14d ago[flagged]
- jjtheblunt 14d ago>. Claude produced the first end-to-end, computer-checked proof of FLT. Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. I'm just old enough to remember Paul Erdo"s and his notion of 'The Book', which he defined to be a book the "Supreme Fascist" (God) had which held the most elegant proofs of mathematical theorems. https://en.wikipedia.org/wiki/Paul_Erdős#Personal_life https://en.wikipedia.org/wiki/Paul_Erdős#Personal_life It would be interesting to see how Erdo"s would name such a huge proof by Claude using Lean.
- mnewme 14d agoDo I miss something? But isnt there the whole code and paper of Kevin Buzzard in the training data of Claude?
- sanxiyn 14d agoYes, but Claude formalized a different proof than Buzzard is trying to, so it helps less than you think. (It certainly helps!)
- EGreg 14d agoSo Fermat’s Last Theorem has been proven a long time ago? By Andrew Wiles right? Is this like Appel and Haken >>> Seymour and Robin Thomas proof of 4CT?
- kzrdude 14d agoFLT was proven in 1995 by Andrew Wiles (with help of Richard Taylor). This is not even a new proof, or at least they don't claim that it is. It's the formalization (in Lean) of an existing proof. That means, they are 'porting' the proof to a theorem proving programming language.
- threethirtytwo 14d ago>The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway). What is even the point? Have claude do it. I'm not trying to be snarky here. I'm being serious. What is the point? This is an important question that needs to be answered. If something is definitively better, why not have that something take over? I know people talk about the importance of human endeavor or the "joy" of doing something. But I don't care for those answers because it's weak. The question is deeper than this. AI is better than us, what is the logical point other than attempting to monopolize human effort even though it is inferior.
- Azantys 14d agoThe whole point was for the formalization to be clean enough so it could be reused in other parts of mathematics as I understand it. 13M lines of AI slop which have never been checked do not sound like what the original goal for such a formalization was. Also Claude didnt prove anything it just translated an already existing proof by Wiles into Lean, so it didn't actually contribute anything other than "Guys we did this thing, look how great our model is!". We never questioned that a printer can print faster than a human can write, but we dont let printers write novels.
- threethirtytwo 14d agoThen why is the guy not cleaning it up. Clearly he thinks it’s done and he’s moving on to do side things. He also explicitly said it went on to do more than what he was required to do. Are you hallucinating? Because huge portion of what you wrote directly and logically contradicts the quotation I wrote.
- OhNoNotAgain_99 14d ago[dead]
- black_knight 14d agoI wonder if any piece of the lean code is in a shape which means it could be contributed to one of the Lean libraries. My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!
- mikmoila 14d ago"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.
- behnamoh 14d agoFor now. That, too, will change in the future.
- educasean 14d agoBy this standard, no computer has ever accomplished anything, because humans built the computer. AI bubble about to burst any second now.
- mikmoila 14d agoHumans built the tool which enabled the result. AI used the tooling for eliminating the dead ends. Yes, I can appreciate the practical value of all this, but IMHO it is not a kind of breakthrough result the article gives impression of.
- johnsmith1840 14d agoA literal rock we carved patterns on and shot lightning into has accomplished something no human has. How much more magical do you want this to be? Tool or not it did something you could never have accomplished.
- glimshe 14d ago"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 Eisenstein ideal to conclude that no Frey curve can have a point of order p>=17. This means that their FLT proof only works for p>=17, however FLT was already formalized for odd regular primes by Best-Birkbeck-Brasca-Rodriguez, and the smallest irregular prime is 37, so it’s all good." My question to any mathematician reading this: does the above make ANY sense to you? I ask that because I can read most technical material related to computer engineering, programming, hardware specifications etc. Even if I don't fully understand all details, I can follow them pretty well. So I wonder if professional mathematicians can look at the above and still make sense of it like experienced software engineers do for computer stuff.
- jovas 14d agoYes, I'm a mathematician. But not an expert on this. While I don't know the specifics, and someone more "in-the-field" than me would recognize all the "named" theorems etc I am aware that there have been minor issues that have come up with the formalization specifically, and that previous proofs for lower values of n were always needed. Though it used to be n=5 and lower needed to be checked.
- CogDisco 14d agoYep. While I'm not focussed on these areas, I know enough from scoping out a "learn about the proof of FLT" course that it's covering all the usual suspects and says the right-enough words. Patching their weaker results with someone else's seem like a good strategy (and I could find the result on arXiv so it isn't obviously hallucinated). This is very different to believing the proof, which would require at least a pass understanding the general approach, seeing that it all actually fits together, then going deeper. At some point you transition to relying on the Lean all hanging together, but as mathematicians we all draw that line somewhere. But yeah, makes sense. Same thing if you saw news on someone's new database technique to improve performance. If they say the right words, don't say the wrong words, and if you cared enough you'd do spot checks proportional to the claim. If pressed you'd examine the source code, and run independent checks. But if smells roughly right, that's a good first approximation.
- deleted 14d ago[deleted]
- maw 14d agoI have discovered a truly marvellous proof of this, which this margin is too narrow bear the load.
- vmilner 14d agoFormalisation of the classification of finite simple groups must be on someone’s ‘moonshot’ list.
- logicallee 14d agoamazing, 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?
- sanxiyn 14d agoLean's three standard axioms are documented in The Lean Language Reference. https://lean-lang.org/doc/reference/latest/Axioms/#standard-axioms https://lean-lang.org/doc/reference/latest/Axioms/#standard-... The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → α The axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = b The quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b)
- auggierose 14d agoI 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.
- margorczynski 14d agoWith how capable and cheap automatic proof verification is becoming I wonder how many proofs assumed to be true by almost all of the math community will be proven false. And not by some marginal easy to fix error by some fundamental flaw in reasoning.
- jeremyjh 14d agoI will not be surprised if the number is zero. It should have already happened if it were possible. Proving that a conjecture is false is very different than what you are proposing. You are proposing an existing proof is simply wrong, that the proof can be checked in Lean, and that no one has bothered to check it yet.
- deleted 14d ago[deleted]
- max979 14d agoPretty wild seeing this get formalized. Remember struggling to even grasp the high-level concepts of Wiles's proof.
- dist-epoch 14d agoLean required 300 GB of RAM, 96 cores, and took hours to compile and check the formalization. Now they have the perfect stress test to hill-climb and optimize.
- dextrous 14d agoOk, let’s get a rabid pack of agents cranking on P = NP? next!
- sva_ 14d agoHmm kind of funny, some years ago someone claimed LLMs can do math, and I replied if it could prove fermants theorem: https://news.ycombinator.com/item?id=33176996#33177939 https://news.ycombinator.com/item?id=33176996#33177939 > Now try to make a computer prove that there are no natural numbers a,b,c; so that a^n + b^n = c^n for any n > 2. > > Shifting the goal posts a bit, aren't we? I guess the goalposts did change a bit, and in a pretty short time.
- kzrdude 14d agoThe OP is about formalizing an existing result, not coming up with a new proof for FLT.
- throw567643u8 14d ago13 million lines of code, a lot of which is new to Mathlib. So it hasn't built on what is already there but synthesised a bunch of new stuff. LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.
- throwaboat 14d agoI wrote a similar DAG-based verifier as a skill a few months ago: https://github.com/sethlei/Warrant https://github.com/sethlei/Warrant . The thing mine has that I didn't see in their's is a verification of the composition rules. Mine also does more than just math.
- cyode 14d agoI saw the 1996 FLT documentary in high school calculus class. For me, it forever cemented that archetype of modern math researcher at the top of my mental “smart” totem pole. It also convinced me I had no interest in that path. Setting aside the grinding work of producing a proof that can only be reached by existing years in the abstract and hyper niche isolation of the problem space (not to mention that you might never discover it or that it DNE), the anguish of the output being a paper or presentation or some other artifact of human symbology (_words_, really) that could at any moment be refuted by a single observation of a single mistake—-that sounded like hell to me. An equivalent high schooler today probably sees things differently, in light of this news and the undeniable implications of LLMs on mathematics. Sturdy autoformalization tooling should with time completely dispel the aforementioned anguish, once our confidence in converting a human proof to Lean/etc. reaches that of a compiler translating Java application language to bytecode. Errata may always exist, but in practice these new methods will do wonders for rigor and peace of mind. (I’m far less confident re novel discoveries. There’s too much chance of derivative findings based on something part of the training looking like genius but really just tiptoeing on the shoulders of humans, whereas autoformalization is absolutely convincing to me as transformative, particularly to check correctness of AI outputted proofs as mentioned in the post.)
- MichaelDairy 14d agoI think Anthropic might the frontier lab hiring contractors through data vendors to formalize mathematical textbooks for them at a rate of 170-200 dollars per hour. This was mainly through Alignerr which has the worst reputation for not paying their contractors. They have been hiring since February as far as I can recall. This is in addition to all the internal people they might have working on this. If they have been formalizing all this work for the past 9 months before having Claude use all this data needed to formalize FLT, then it wouldn't be Claude formalizing FLT in just 11 days. Same with the upcoming results they will claim Claude came up with, but in fact they have been hiring frontier researchers working on very niche topics through Micro1. It's all a marketing ploy before their IPO.
- herbcso 14d agoSo 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 just feels like a LOT of code to be comletely error-free... What am I missing here?
- twiceaday 14d agoLean 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.
- throw-qqqqq 14d agoGreat explanation. I’ve heard this referred to, as The Formal Specification problem. From https://en.wikipedia.org/wiki/Formal_specification#Limitations 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.
- thevivekpandey 14d agoIn lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type. If the compiler certifies that the code indeed produces a term of that type, then the proof is correct. So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really) (2) Lean compiler is correct
- gorgolo 14d ago> 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”?
- Goofy_Coyote 14d agoFor math illiterate people like me, my understanding is that FLT was already proven, but the proof was beyond complex, certainly for mere mortals like me, and now Claude has codified it, correct?
- andychiare 14d agoWe are in the context of "who verifies the verifier?" :-)
- mettamage 14d agoFirst of all, this is an amazing result. Second, I'm not too surprised, given all what has happened before. The thing is: LLMs are not grounded in reality enough as much as we are. Using Lean is exactly what that is: grounding LLMs in reality. We have (at least) 30 FPS vision, and can detect 5 ms audio delays, we do that in real-time. LLMs have access to some images and large amounts of text. Their propensity is to predict the next token. So the propensity to be additive and just say something (aka predict the next token) is higher than predicting something to stop. If LLMs would have: - 30 FPS vision - similar hearing ability - an ability to feel their lived experience - consequences to their "life" They'd be making more intelligent decisions than they are doing now. Simply because they have more context. Because in this sense, we have a lot more context than LLMs. Yet, I see people sometimes treating them as if they are at the same level as humans because their intelligence is similar. And that might be true, but where they get their data from is vastly different. Given our tasks, they are at a disadvantage. They need to sense more of reality. Have fun sharing the room with these digital intelligences. Given the topics they can consume, they are already better generalists than any individual. I might be wrong of course, I'd love to meet any individual that's a better generalist than an LLM.
- amelius 14d agoThey should let AI work on it until the proof fits in the margin of a page.
- FartyMcFarter 14d ago5 minutes later, the AI concludes the best strategy is to start a universe simulation and let Fermat write the proof in a margin. Recurse.
- amelius 13d agoYeah they tried that, but the proof didn't fit.
- jeanmichelselli 14d agoI'm a mathematician and I'm not sure one should believe those results right now.. An automatic formalization requires a system of logic rules to be applied, which is not something LLMs are great at (remember the Apple paper a while ago?). I'm very curious to see how the community will react after the initial hype.. so far, it's being quite disappointing..
- Smaug123 14d agoThe LLM is not the thing applying the logical rules. That is instead the deterministic system Lean 4. (Also that Apple paper was garbage even when it was written, assuming you’re referring to The Illusion of Thinking, and LLMs have got much better since.)
- auggierose 13d agoKevin Buzzard is a mathematician as well, and he thinks it's ok. I am a mathematician, too, and I know it is ok. What I find fascinating is how little mathematicians still know about this. But I am used to that attitude towards interactive theorem proving for quite some time. The difference now: if you don't adapt, you are obsolete and done for as a mathematician.
- vitriol83 14d agoi find this and other efforts from anthropic somewhat antisocial. technically they have achieved their goal, but in a way which does not benefit mathematics or humanity. Kevin Buzzards headline goal was to formalise FLT, but i’m sure the real aim was to create a formalised library of mathematics which is comprehensible to humans. By solving these famous problems by brute force, they are disincentivising the important work of making it digestible for everyone else, and so in my view this work in particular has negative societal value.
- auggierose 13d agoMaybe society has the wrong values. Maybe society needs to rethink incentives. Maybe society is somewhat antisocial.
- vitriol83 13d agoyes society has let the trillion dollar company down
- auggierose 13d agoYou can say that American society made OpenAI and Anthropic possible. No other current society would have. Suddenly, formalisation of math is becoming cheap. That's not a problem, that's the goal, and it is here much earlier than expected. That's not antisocial. That is scientific progress. (I swear, did not use an LLM for this)
- vitriol83 13d agoYou're stating it's not a problem- but I'm giving you a reason why it is. This is serendipitously mirrored by a recent post from Terence Tao on Mastodon (https://mathstodon.xyz/@tao/117207856734787448 https://mathstodon.xyz/@tao/117207856734787448) In most cases in pure mathematics, the problems are posed not because we desperately want the solution to these problems in and of themselves, but because we have seen from past experience that human-directed efforts to solve these problems tend to spur further development of the field through the efforts to solve such problems, and then to digest any partial or complete solutions that emerge for further insights. Prematurely solving the problem by purely AI-powered methods - particularly without full transparency into the solution process - can contaminate this process to the point where it actually becomes a net negative for the progress of mathematics as a whole.
- satnhak 13d agoI used to attend Kevin's Number Theory seminars at Imperial College many years ago and he's both a first rate mathematician and a very nice person. His blog has got me interested in maths again. Considering how pro AI he is and that he's been working on this problem for such a long time I'm a bit disappointed that Anthropic didn't involve him directly in this work. However, I think it's important to remember that without all of the work Kevin and people like him have done, the machines wouldn't be able to do this.
- imranq 13d agoNote that this proof while impressive does not add any value to mathematics as a human pursuit. But it does show we can throw these LLM beasts at much gnarlier problems than we could have imagined previously. Maybe even formally verify papers the day they are posted? I'd love to see an e2e compiler or OS kernel verification or Full-stack chip design with formal equivalence checking at each stage that would be pretty cool. What else is interesting is how they staged this problem : (a) maintain an explicit DAG/roadmap of sub-goals rather than one flat prompt, (b) separate statements from proofs so many agents can work on different nodes without stepping on each other, (c) keep a natural-language index alongside the formal one so search/reuse works... I feel like this is the future of long horizon agents and how you can do work that's making the most of every agent. This approach will likely be baked into the next versions of coding harnesses
- jebarker 13d ago> Note that this proof while impressive does not add any value to mathematics as a human pursuit. I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.
- mkehrt 13d agoI enjoyed this Terence Tao post the other day. The relevant quote is > one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?" And later > But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided by any human expert in the field X resides in, has created an unprecedented divergence between the production of answers, and the production of insight, to the point where the two questions have become _negatively correlated_: https://mathstodon.xyz/@tao/117208618508728654 https://mathstodon.xyz/@tao/117208618508728654
- 13d ago
- HarHarVeryFunny 13d agoLet's hope Lean really is bug free. https://arxiv.org/html/2609.04170v1 https://arxiv.org/html/2609.04170v1
- antsou 12d agoAI should prove it the way Fermat imagined ...