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

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-the-kernel-soundness-bug-hunt/ 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.