logoalt Hacker News

gowldyesterday at 11:06 PM0 repliesview on HN

Why should you trust that the relatively small core of Lean is correct?

The core of Lean got a lot less correct when a well-meaning AI system probed Lean for corner cases (bugs) that would "prove" a false conjecture. Corner cases so arcane that no human exploit in a proof. Basically, humans are too stupid to break human-created Lean, but the AI is not.