Can you hear the shape of a Lean soundness bug? A wager.

IntroductionThe advent of powerful but untrustworthy artificial intelligence has enlivened a formal methods summer, in which formal methods—historically, the domain of meticulous academics—are suddenly attracting tens to hundreds of millions of dollars in venture capital; being touted by big-labs as proof that their “proofs” are correct; getting integrated into agent pipelines; and becoming load-bearing for various AI safety proposals. Right now, like, right right now, when we speak to employees...