Hacker News Reader

How long until we find out that some AI has quietly buried an exploit in Lean to cheat at proofs?

Simpler to exploit a soundness bug than introduce a back door I would assume