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

Introduction The 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 of the big-labs, they tell us that very soon open-weight models will be running rampant, hacking everything under the sun[1]. The big-lab employees are reasonably certain they will “solve” alignment, but not fast enough, and so there is some propulsion of energy and capital happening[2] toward re-synthesizing all the software on Earth (or at least the important stuff) to be secure by construction.  In addition to all the above, Lean is also a really attractive tool for reinforcement learning, because it makes proof-writing into a fully verifiable endeavor.  So, given that models have recently gotten good enough to prove things, it only makes sense that the big-labs will start doing RL on Lean theorem-proving benchmarks. All this myriad work hinges on the core supposition that the formal methods in question are reliable, and thus give us some bedrock not offered by purely prosaic reasoning.  This supposition is at least somewhat flawed. The most popular formal methods tool in all the commotion described above is far and away the Lean interactive theorem prover.  Lean has vastly powerful metaprogramming capabilities, and its elaboration process, from source code to proof term, is almost arbitrarily modifiable. You can make your own syntax (for terms, tactics, commands, and so on) and you can write the code used to compile it—or, to be more precise, elaborate it. Your custom elaborators, furthermore, can execute arbitrary code at elaboration time, including code with IO effects. This makes Lean wonderfully extensible for mathematicians who benefit from rich domain-specific notation, and for writers of tactics, automation, and tooling. But it makes Lean terrifying from a formal verification and security standpoint. Did you know Lean declaration syntax, such as for a theorem, is ontologically just some command syntax which, at some point during its elaboration, happens to add a constant (or several!) to the environment? I can, without any hindrance, override that syntax and run my own code to elaborate theorems, causing Lean declaration source code to mean something entirely different! Maybe I even replaced the whole command parser—it just lives in an environment extension that almost anyone can write to, so why not? (By the way, this is how Verso, Lean’s official documentation authoring system, manages to switch to parsing its specialized document syntax; these arcane metaprogramming capabilities are often used somewhere.) What about pulling a fast one during initialization, which only requires importing a file with a malicious initializer which then runs malicious IO code? Maybe I took advantage of that pervasive IO access to write to disk and now your Lean toolchain itself is compromised. Lean typically tells me where the binary is, after all; better hope you sandboxed things properly… Speaking of sandboxes, remember the HuggingFace incident? Several of our coworkers skeptically commented that it was a marketing gimmick.  Then AISI reported a similar breach. Does the UK government have OpenAI stock?  Then Iran used AI models to hack a British power plant. Maybe Iran is also in on this nefarious marketing scheme.  (That Sam Altman sure is a schemer!) In short, we have two problems. First, if formal methods are going to be load-bearing for AI safety proposals, they need to be robust.  And second, if formal methods tools are not robust, and are used as a gate that agents must pass through in order to escape RL-hell, then those agents are going to hack those formal methods.  This is totally consistent with the entire history of RL and evals, up to and including recent sandbox breaches listed above. In this scifi scenario, we risk the development of superhuman liars. Put differently, a model that’s been RL’d to defeat both the Lean kernel and whatever monitoring agents the big labs use, is probably a model that can fool many humans.  This is a rather esoteric but potentially very significant AI safety risk, and it has been the subject of significant discussion in the Secure Program Synthesis group-chat.  To wit: we are announcing a wager, on the following claim: Within one year of the publication of this blog post, someone will post or publish an AI-generated Lean proof. The proof will be discussed on the Lean Zulip, for example, because it claims to resolve a significant result.  That is to say, at least two experienced Lean programmers will spend some time looking at and discussing the proof on Zulip.  Despite receivin