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.

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.

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.

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.

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.

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!

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