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

71–80 of 526 posts

Re: Formalizing Fermat's Last Theorem

#71

Post by stratos123 »

hyperhello wrote: post #53
prometheus1992 wrote: post #50

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

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

Re: Formalizing Fermat's Last Theorem

#72

Post by simpaticoder »

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?

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

Re: Formalizing Fermat's Last Theorem

#73

Post by hyperhello »

epgui wrote: post #62
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.

Is Lean a DSL? I’d argue it’s a general purpose programming language that excels at proofs.

Well, 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.

Re: Formalizing Fermat's Last Theorem

#74

Post by davmre »

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

Re: Formalizing Fermat's Last Theorem

#75

Post by tinfoilhatter »

Vakaiser wrote: post #9

We'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 agi…

It'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.

Re: Formalizing Fermat's Last Theorem

#76

Post by tossandthrow »

Jaxan wrote: post #70
tossandthrow wrote: post #63

Earlier quoted context omitted.

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

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

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

Re: Formalizing Fermat's Last Theorem

#77

Post by kingstnap »

KaiserPister wrote: post #39

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

The AI labs have out considerable effort in trying to find and patch lean exploits. They explicitly set agents and have them try to prove false.

> Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime

https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...

They found several bugs and they have patched them. Lots of work going into making sure lean is sound.

Re: Formalizing Fermat's Last Theorem

#78

Post by 3192987 »

voxl wrote: post #41
lseplot wrote: post #10

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!

It'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.

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

Re: Formalizing Fermat's Last Theorem

#80

Post by simpaticoder »

bjourne wrote: post #36
jrflo wrote: post #17

Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?

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

But 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?
Post reply on HN