Hacker News Reader

Comment by KaiserPister | Hacker News Reader

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.

Some argue that Lean breaks a few type-theoretical properties. See full discussion here:

https://github.com/rocq-prover/rocq/issues/10871

This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.

We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)

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

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

No, comparator does check the entire closure

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

That must have slipped through Kevin Buzzard's review, which is not entirely unplausible with 29500 theorems to verify...

I think they should spend another few billion tokens and let agents try to disprove any of those statements or links between them. Then I'd be a lot more convinced.

You just have to trust the statement and the lean compiler, not the proof. The compiler certainly still has remaining bugs, but I have never seen a bug leading to a false proof in good faith, only via obscure meta programming tricks. The nice thing is that the multiple versions of the compiler are constantly being stress tested. Still, there is plenty of work that could be done to make the compiler more trustworthy / easier to verify.

This being 13M lines of entirely agent-generated code, we can't be certain it's written in good faith and doesn't actually exploit some weird metaprogramming trick. The agents' goal was to write a proof that Lean prints "correct" on, not to check that the proof of the FLT was valid (which they wouldn't be able to do anyway).

It's not impossible, but I also know of no instances of an AI being told to prove something in Lean and exploiting such tricks. Surely Anthropic also had some agents looking for issues with the generated proofs. Personally, I am also comfortable trusting Kevin Buzzard, who was leading the human team aiming to formalize FLT and discussed this a bit on his blog.

Finally, the good thing about Lean is that if anyone ever finds a new compiler bug (which, by the way, are being searched for extensively using AI), you can correct the bug and recompile any old proofs of which you are suspicious. Any tricks in a false proof must be exploiting a bug in the Lean compiler, so as we increase trust in the compiler over time we also increase trust in every previously compiled proof.

I agree it's not a 100% guarantee, but in this case the human proof is well-understood and written about by many experts, so I think Claude had plenty of material to work with. Even if the task was enormous, I don't think any of the individual steps are out of the scope of what we have seen from current AI tools.

Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.

Nope! :(

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!

Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.

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

do we know if claude's formalization is built on top of zfc and not zfc+extra?

zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.

Within a given inference system, one can define concepts. This doesn’t add any axioms. It is, in essence, just a way to abbreviate things.

ok, you now added some unknown inference system in addition to zfc

No, it is the same inference system. They are just abbreviations.

and what is that system?

ZFC

zfc is a bunch of axioms and not inference system. It is commonly assumed that it is built on top of some unspecified first order logic which commonly assumed to include bunch of inference rules. There is no ground truth in my understanding where this all is formally defined.

If you want to use “ZFC” to refer to the axioms without any rules of inference, I guess you can do that, but when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.

> when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.

its bro-math. In formal math you need to be specific what inference system you use. There are many of them. Then you need to have formal proof that in that system you can derive concept of function and then think about question if it won't make paradoxes and contradictions with ZFC.

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

Reply to sibling - lean4 doesn't rest on ZF or ZFC. https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Co... However I believe an equivalence of power has been shown between the two.

Roughly, yes. See B. Werner (1997) “Sets in types, types in sets”.

There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless.

You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.

It would be fun to play with this Anthropic/Lean formalization under different axiomatics.

> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.

Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.

If you start with "I'm not a strong expert" maybe you should stop continuing saying wrong stuff. What you just wrote is completely wrong.

support your point with explanation or be ignored :-)

Godel proved that any system expressive enough to produce an arithmetic is incomplete. He initially proved it for the peano axioms but then it got generalized. ZFC can produce an arithmetic. Also, before being arrogant and demanding explanations, you should give them first for your claims

> expressive enough to produce

you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.

why should they be obvious? they are derived and have been thoroughly proven.

looks like we are in disagreement

A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong

you are entitled to have your opinion :-)

and you are entitled to talk about maths while rejecting maths

coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants.

I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another.

ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it. Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.

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

> Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.

I am aware, also I am not sure why you wrote all of this. Your unknown to me "first course" claims to be some authority of formalization purity?

Because you wrote:

> what are exactly rules, which could be separate topic of research, this detail is skipped

I am now confident you’re a troll, though, so I am going to bow out.

I referred to specific definition in wikipedia. Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.

What are you nerds fighting about please explain

That increases the likelihood that they are right.

> support your point with explanation or be ignored :-)

Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.

https://math.stackexchange.com/questions/1366560/why-does-g%...

https://math.stackexchange.com/questions/1090437/how-to-prov...

imo, those two links are example of rather low quality weird math discussions, but you can keep your opinion

> imo, those two links are example of rather low quality weird math discussions, but you can keep your opinion

I've seen a lot of bad faith on this site, but none exceeding that.

> Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC.

https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...

> interpreted

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

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

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

> you just build some sets to represent numbers and make operations that act the same way as arithmetic

which is already "just" some non trivial problem(there is no "operations" in set theory), and we are discussing if it is achievable.

You make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.

No, once you start formalize this, it becomes complicated. There is a reason why looks like there is no "peano can be derived from zfc" theorem which would close dispute, and my opponents need to throw links on bro math from stackexchange in this discussion.

Per https://en.wikipedia.org/wiki/Peano_axioms#Set-theoretic_mod...

> The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.[15]

If you're going against the general consensus you should present something more than nebulous assertions that it's wrong.

Obviously citation from wikipedia can't be considered as replacement of math proof.

> If you're going against the general consensus you should present something more than nebulous assertions that it's wrong.

burden of proof is on the one who claims something exists.

That is wildly wrong.

ZFC has greater consistency strength than PA.

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

zfc doesn't have functions, so you are building something new on top of it.

Also, I am not sure successor function is enough for PA.

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

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

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

Can you cite where did you get this?

As I have said a few times now, you should read any first course in set theory. I’m quoting my third-year notes from Cambridge there, but essentially every intro to set theory will say the same. (I’m sure someone will find a single counterexample that does it somehow differently.)

Your third year notes from Cambridge has very low authority to me

Formally, a function f is a relation between sets A and B such that, for all x in A and u,v in B, f(x) = u and f(x) = v implies u = v.

It's just a definition. Authority is, as the parent suggests, any introduction to set theory.

> Formally, a function f is a relation

discussion was if zfc has functions at all, not sure why you put relation here.

The guy's remarkable response makes clear that he's a clueless troll.

Interestingly, in his ICM 2026 lecture, Terence Tao specifically mentioned that Lean is not based on ZFC.

Lean is based on Type Theory not ZFC.

I always wanted to, say, look at any theorem and see what axiomatic it requires. Or in other way, see the theorem tree like in the article under a different set of axioms.

Of course, for some results there are proofs discovered only under one axiomatic, but it's true under some others as well, just the proof wasn't discovered yet.

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.

the Nanoda type-checker for Lean is ~5,000 lines of Rust:

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

...and some thoughts on putting stuff in the kernel:

https://lawrencecpaulson.github.io/2026/07/30/Collatz.html

Reply on news.ycombinator.com