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

kingstnap 2 hours ago | parent | next [-]

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.

▲

Jaxan 2 hours ago | parent | prev | next [-]

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

▲

Smaug123 2 hours ago | parent | prev | next [-]

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.

	▲	jmusall 26 minutes ago \| parent [-]
		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.

▲

jmusall 16 minutes ago | parent | prev | next [-]

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.

▲

andriy_koval 2 hours ago | parent | prev | next [-]

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.

▲

deepsun 23 minutes ago | parent | next [-]

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.

▲

andriy_koval 13 minutes ago | parent [-]

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

▲

Almondsetat 3 minutes ago | parent [-]

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.

	▲	andriy_koval a minute ago \| parent [-]
		support your point with explanation or be ignored :-)

▲

ajs1998 an hour ago | parent | prev [-]

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.

	▲	andriy_koval 23 minutes ago \| parent [-]
		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.

▲

tossandthrow 2 hours ago | parent | prev | next [-]

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.

▲

Jaxan 2 hours ago | parent | next [-]

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

	▲	tossandthrow 2 hours ago \| parent [-]
		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.

▲

Jblx2 2 hours ago | parent | prev [-]

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

▲

dist-epoch an hour ago | parent | prev | next [-]

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

▲

holmesworcester 2 hours ago | parent | prev [-]

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!