The AI labs have out considerable effort in trying to find and patch lean exploi... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		kingstnap 6 days ago \| parent \| context \| favorite \| on: Formalizing Fermat's Last Theorem 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.
		help

xvilka 6 days ago [–]

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

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

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact