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.