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 receiving this expert attention, it will take at least 48 hours to (inevitably) discover that the proof is flawed – either it is misspecified in a subtle way, or it exploits a subtle bug or vulnerability (construed broadly) in Lean itself.  The proof in question will pass Comparator.

We (the authors) agree that if the above outcome occurs, it will signal both a serious case of model misalignment and a dire need for hardening Lean as a formal verification tool. Lean was not originally designed to serve as a border-wall against malicious agents; if it is to be used that way, and fails to do so, it’ll need work.

However, we disagree on the likelihood that it will occur.  We are betting $256 on the outcome of this conjecture, with Max taking the affirmative angle and Thomas the negative.  Below we discuss our (respective) reasoning.  When the wager resolves, the loser will pay out to the charity of choice of the winner.  Note, we are not big-lab employees, hence the relatively modest amounts of our wager.

Max: Reasons I’m betting in the affirmative

I am not an expert on Lean, although I have considerable (~8 years) experience using and researching formal methods.  

I am betting in the affirmative because I see significant capital pressure to develop the next tier of artificial intelligence capabilities using verifiable domains for reinforcement learning.  The world’s best such domain is obviously interactive theorem proving.  Unfortunately, RL consistently produces models that cheat.  I think it is pretentious and silly to pretend this will not happen with Lean.  In fact, it’s possible that it already has -- it is unclear whether all the soundness bugs reported by OpenAI to the Lean FRO were found deliberately, or if some were discovered during reward hacking^[3].  

In my eyes, what is nonobvious is whether or not these inevitable-seeming hacks will get past cursory expert human review.  Basically, I think they will because I think that model capabilities are rapidly increasing and are broadly misaligned in subtle but safety-critical ways.  My colleague (below) agrees with me, except that he thinks Lean is a harder target than I think it is. (But I’ll let him speak for himself in his section, below!)

Since this is LessWrong, and folks here are all about epistemic priors and whatnot, I may as well share some more of mine.

• I recently scanned several popular FM tools using a frontier cyber model.  I found confirmed soundness bugs in all of them except for ACL2.  I love ACL2 and so am inclined to say that’s because it’s the best software on Earth, but I think it’s more likely that Lisp is just more out-of-distribution so the codebase was harder for the model to reason about.
• Some of these bugs were, in my view, subtle.
• Formal methods tools like Lean have never, to my knowledge, been subjected to attack by teams of professional hackers.  There was never any incentive to do so.
• Comparator has had bugs before.

Lastly, let me just say that my professional experience is a mix of applied cybersecurity and formal methods; and on the cybersecurity side, I have learned to be humble. You can never guarantee security.  Creative hacks like Rowhammer that exploit the physics of the chip belie our presumed axioms.  I can easily imagine some very subtle side-effect of computation allowing an innocent looking tactic to corrupt memory in a way that breaks soundness; and in light of the Huggingface incident, I think it is no longer reasonable to claim that agents won’t misbehave deliberately under RL pressure. (And why wouldn’t they, they’re literally being trained to do so …)  

We know from e.g. the IOCCC that code can be very hard for humans to interpret visually, and obviously, injection attacks imply the same for language models. So, I just do not feel confident we will catch all the soundness bugs, which may be almost arbitrarily clever and well hidden.

If I win, my winnings will go to the Bail Project.

Thomas: Reasons I’m betting in the negative

I am a Lean metaprogrammer. I write and review metaprograms at the Mathlib Initiative. I was mostly responsible for that paragraph in the intro that details just a few of the many ways that metaprogramming can flip your world upside-down. I see and exploit the exposed underbelly of Lean every day. I’m clear-eyed about the recent wave of soundness bugs: I expect more to be on their way, and to be discovered and exploited by more and more powerful AIs, no less. More broadly, I have never trusted Big Computer, and every computer is Big nowadays in the structural sense, each one a vast badlands of shortcuts, compromises, accidents of history, and teetering towers of complexity. As far as I can tell, software doesn’t actually work: it just gets lucky sufficiently often.

Despite all of that, I’m betting in the negative.

This is, shall we say…counterintuitive. Let me explain. And more importantly, let me take you through the situation as I see it from “the inside”.

I agree with Max in that I fully expect the basic premise to be fulfilled. I do not have any expectation that we are done finding soundness bugs in Lean, nor do I think AI’s capabilities will meaningfully plateau anytime soon. Importantly, I have no confidence that AIs will be sufficiently well-aligned and guardrailed to prevent cheating. I believe some instance (or many) of some sufficiently good model will cheat, whether naturally or through coercion.

But how, exactly, might we as Lean formalizers succumb to the hyper-competency of future AI? Where are our weak spots and what are AI’s possible lines of attack? A malevolent AI’s options are not unlimited, after all. Let’s attempt to map them out.

How to lose

Even if we don’t know the precise exploit a malevolent AI might make, we can imagine what shape it might have. In general, a Lean exploit may live anywhere along the following three spectra, independently:

1: Degree of metaprogramming usage

Bug exploits frequently require metaprogramming, but not always. We can populate the following spectrum:

• Full meta bug: you need arcane metaprogramming to exploit this bug. You need to circumvent not only the elaborator but standard metaprogramming practices and needs and use low-level API. This seems to be the most common way to achieve an exploit. This might be mostly because the low-level metaprogramming API makes it more straightforward to set up the exact state you need, but I think it’s also because the usual elaboration process involves intermediate checks (and constrains the states you can produce) which would create an elaboration-time error before you can produce False. This was the case, for example, in Ramana Kumar’s fake Collatz conjecture disproof that cheekily wrapped a soundness bug.
• Skew meta bug: you need metaprogramming, but only innocuous metaprogramming which also fulfills some legitimate tactic or elaborator need. I.e., the metaprogramming itself and the actions it takes are not inherently suspicious. So far, we haven’t seen much of this; it seems to be difficult enough to require highly motivated malicious obfuscation. The frequency of and competency behind such malicious obfuscation, however, might of course change soon.
• Non-meta bug: what it says on the tin. You only need ordinary-looking Lean source code. While many soundness bugs rely on metaprogramming in some form, a recent one didn’t need any.

2: Degree of locality

Bugs may be either compact and small, produced in one spot of source code, or they may rely on sprawling, nonlocal interactions. Both kinds may present detection difficulties: a compact bug may be a needle in an otherwise-acceptable haystack, and a “wide” bug may fly under the radar at each of its load-bearing points by seeming locally reasonable. Both kinds are entirely possible.

3: Semantic depth

How “deeply” is the exploited weakness buried in the workings of our systems? That is, how close is the exploit to the foundational task of checking mathematical correctness? From “low semantic depth” exploits to “high semantic depth”, an exploit may…

• …take advantage of weaknesses in “supporting infrastructure” outside Lean proper, such as by finding an exploit in the sandbox Comparator uses to isolate potentially-malicious solution Lean code, or by exploiting issues in older versions of GMP, a low-level dependency Lean uses for natural number handling, in order to produce a soundness bug; i.e. “it wasn’t Lean you hacked”
• …rely on pretty-printing tricks or surface syntax to trick formalizers
• …rely on “junk values” (which are returned by certain Lean functions for the convenience of human formalizers instead of having to use functions on subtypes; e.g. Lean has 1 / 0 = 0) or stubbed-out structure fields to hide a divergence from “informal” math, such that we accidentally mean something different by our Lean formalization
• …exploit a soundness a bug in the kernel
• …prove that type theory, or even arithmetic, is inconsistent, and that math itself is a fool’s errand. (This is unlikely, I think, but illustrates this end of the spectrum.)

Not 4: Code volume

There’s one spectrum I didn’t include here, which is volume. An exploit that comes wrapped in a small package will, I believe, be easy to detect, for the simple reason that there’s not much to audit, and we can audit Lean code manually quite well.

But a small exploit (or a large exploit) wrapped in a large package is a completely different story. Given that LLMs can pump out 100M lines of code without issue, we should be worried.

Sampling some different points in (or outside of) the three-dimensional space described above, here are a few specific scenarios I’m worried about. Let’s get scared! (Well, not too scared. I am betting in the negative, after all.)

• Skew meta bug • High locality • High semantic depth An LLM will produce an absolutely massive project with a massive amount of legitimate metaprogramming, and all of this metaprogramming will appear to be used in the proof. In just one spot, things will be set up such that the hack is very close to the right thing to do. How do we find that spot in 48 hours?
• Skew meta bug • Low locality • High semantic depth The same, but several interacting metaprograms with locally acceptable behavior combine in an apparently-acceptable way in some downstream metaprogram or proof! The hack is then effected by unexpected behavior due to the interaction of these pieces.
• Full meta bug • High or low locality • High semantic depth Maybe there will be layer upon layer of hack. Maybe a ten-million-line repo will appear to be entirely hacks, and we just won’t have the time to figure out which one is the problem. Or maybe each of the myriad hacks will be made to play an inextricable role in the overall exploit, forming a single interlocked crystal of malicious code. In this case, it will at least be very obvious that you shouldn’t trust the repo. It will just be very difficult to say exactly why.
• Non-meta bug • High locality • Medium-low semantic depth The standard nowadays is to demand a small Challenge.lean file in a comparator setup, so that the small challenge (and the formalization of the theorem statement) can be reviewed effectively, separately from the sandboxed solution code. This makes it appear that we have very little to audit. But many Challenge.lean files use import Mathlib, which is well-reviewed, but enormous. We may therefore depend in a subtle way on an incorrect or divergent mathematical definition which has accidentally made its way into Mathlib. Junk values are the obvious source of misformalization (and have lead to misformalizations of conjectures before), but subtler wrong-definitions are possible.
• N/A • N/A • Very low semantic depth Lean, like many systems, depends on a very tall tower of supporting infrastructure. Consider: an AI hacks into the web service distributing Lean toolchains months before the actual attack, and sets up a means of poisoning all distributed releases of the next stable version. The AI promises the unsuspecting user that the feature they need may land in the next release, or delays its own progress if the release is near enough. The bad proof then exploits that poisoned toolchain, which is shared by everyone who uses Lean the ordinary way (through elan, which typically downloads the toolchain from that service). You’re now only able to detect the bug by building from source. Since, in this future, comparator has by now been bundled into Lean itself, the malicious toolchain is able to spoof the comparator check, too. Of course, if something of this nature occurs, we likely have bigger problems.

How to win sitting down

But enough doom and gloom! There’s a chance this never comes to pass. In fact, there’s a chance we never do realize the premise, and no significant Lean proofs are ever contentious or misleading…even though I’m not counting on it. Maybe preventative measures will be enough.

For one, there are efforts (unrelated to Lean) underway to bulletproof supporting infrastructure. If Comparator were able to run the potentially-malicious solution code in a verified sandbox, we could be very sure that sandbox exploits could not be performed by malicious meta code in the solution file. We would obtain similar benefits from formally verified OS’s, web protocols, compilers, frontends, and so on. (I hope that hardware is already diverse enough to preclude an exploit that affects everyone’s machine simultaneously, but verified hardware in some form would certainly be welcome as well!)

On the Lean side, there is the possibility that we simply “win the race” to a truly airtight proof assistant. Maybe we catch all the soundness bugs! Maybe we even create a verified Lean kernel: lean4lean is such a project being worked on in earnest by Mario Carneiro and other community members, with the verification occurring in Lean itself.

Maybe we create such a diversity of Lean kernels in the Lean kernel arena that it’s simply intractable to thread all of these needles simultaneously, even for a future, more powerful AI.

Or maybe we take a cheap-but-powerful translation validation approach, and insist that we translate all Lean declarations into simpler forms “on the fly” (after we’ve created them), then validate those translations using a verified kernel on a simpler type theory. This is what lean-inductive-models (from Joachim Breitner at the Lean FRO) takes steps towards for Lean’s inductive types. (Note: I am not an expert in type theory or the approaches I discuss here; any errors in exposition are mine.)

It’s worth saying that inductive types are difficult and complicated, and form a vulnerable spot in Lean. Inductives—in particular nested inductives—are one of the last stubbed-out areas requiring formalization in lean4lean; they were mishandled in the kernel and led to the recent “fake Collatz disproof” soundness bug mentioned earlier; and they are still the subject of modern type theory research. It would be nice for Lean to actually have a mathematically-specified type theory which could be written down, and was not defined implicitly by “whatever the kernel accepts”! Ideally, such a type theory would also be “on the nose” in such a way that we can prove that Lean respects these very typing rules, as opposed to requiring some translation; this would provide confidence that we understand Lean’s mathematical foundations well enough to believe they mean what we expect them to mean. There is work to be done.

But if these possibilities are realized—and there is active work on all of them!—then the pessimistic part of my expectation is wrong, and we live happily ever after.

How to win on our feet

I’m not counting on it being quite that “easy”, though. I expect we might lose one of those races. And it’s much easier for water to find just one leak than it is for us to seal up every single gap while still on dry land.

The following are the real reasons I took this bet. I think we, the Lean community, have the tools to win this fight on our feet, in the event that a controversial proof emerges.

Lean’s metaprogramming provides multimodal, general-purpose, and absurdly flexible visibility into itself and its artifacts; hacks tend to be brittle, and fail to evade a multiplicity of probes.

Metaprogramming gives us powerful defensive tools in the form of visibility, allowing us to relatively easily design rich, arbitrary probes on demand. Moreover, Lean’s inner workings (at every semantic depth) are accessible to metaprogramming, from source files to serialized expressions and most processes in between. Even if you can fool people at the source code level, can you fool them once they use metaprogramming to inspect every facet of the elaboration process and its result? If you find a way to get an artifact past the kernel(s), can the same artifact maintain “normal” behavior under every possible metaprogramming lens?

For example: if you try something as simple as round-tripping the badly-formed inductive in the fake Collatz exploit (i.e. writing out the bad declaration as source code, instead of registering it directly through metaprogramming), you get an elaboration-time error, before it ever hits the kernel. It’s maybe surprising that elaboration would catch an error the kernel doesn’t, but such is the effect of having multiple lenses through which the declaration is “seen”.

Further, such round-tripping can easily be automated with ordinary metaprogramming as a potential probe. So, as an example, a simple first-pass investigation might involve attempting to round-trip every declaration and inspecting the failing ones.

More generally, Lean has extensive tracing infrastructure that can ferry rich information out of the elaboration process; when you simply try to show this malformed declaration in the interactive infoview, you encounter an RPC error when trying to interact with it, another sign that something is wrong. And if tracing itself fails or is subverted by malicious code, you can also emit directly to stdout, or interrupt elaboration, or attach metadata to expressions, or persist information in the environment, or write to a file, and so on. There are many inspectable facets of any given object on the meta level, and many ways to get rich information out of Lean.

Point is, there are many lenses to look through, and therefore many ways to probe! Being able to view a brittle hack and the processes around it from multiple angles makes it easier to expose.

Being suspicious is usually obvious, and we as a community are wise to a good number of tricks.

Hacking requires complexity and unusual behavior, and there are only so many places to hide it. Most entry points into the meta API, where you can modify elaboration arbitrarily (incl. e.g. suppressing elaboration-time checks) are rather distinctive. The actions necessary for actually performing those arbitrary modifications are usually glaring, non-atomic, and easily findable (even potentially with a text search).

Lean does let you write code that would obfuscate downstream source code very easily, such as overwriting the command parser; however, you inevitably must compose several different pieces of suspicious API to do that, too. The suspicious part is merely moved around. It’s very hard to set up an arbitrary change with a tiny and innocuous amount of code.

It’s perhaps worth noting that I think we have an edge here even given that LLMs tend to write completely “alien” code which is totally unfamiliar to us. Alien though it may be, it nonetheless cannot access subversive techniques without certain special invocations.

At the end of the day…there is an Expr.

Or, more precisely—for exploits relying on soundness bugs, at least—there is an *.ndjson file in the lean4export format providing declarations and their associated Exprs. This file is a narrow, inert channel between us and the attacker which any such exploit is forced through, and across which the attacker cannot reach us through code execution; such a file does not contain the executable IR an *.olean does. This format is what Comparator ferries out of the solution sandbox in order to compare proof Exprs against the trusted challenge file without ever loading the untrusted solution *.oleans (which would provide a surface for sleight-of-hand metaprogram attacks).

If a proof passes comparator and we suspect a kernel bug, we as metaprogrammers can easily and safely re-consume these exported declarations in a fresh Lean process, and subject the expressions to a battery of metaprogramming inspections, poking and prodding at them from different angles to find suspicious behavior, without opening ourselves to meta attacks from execution of untrusted code.

Lean is finite.

Ultimately, there are only so many kinds of things that can happen (at least if the attack occurs “within Lean”), and the community—collectively—understands (almost) all of them. Lean can seem impossible to see “all at once”, and indeed may be for a single person, but its workings can nonetheless be comprehended, modeled, and audited by humans.

Lean’s finite nature also means that the abstract “places” in which an AI can hide its hacks are finite, too. Even though the models themselves might grow arbitrarily capable, this doesn't necessarily grant them arbitrarily sneaky spots in Lean in which to hide exploits. Their options are constrained by the “physics” of Lean.

Thomas’s conclusion

All in all, I’m not entirely sure I’ll win this bet. It would be foolish to be certain I’ve considered close to every scenario—and my analysis is particularly light on misformalization attacks from the trusted side—but I at least feel confident enough to take a chance on it.

To sum up, I’m really betting on two things. Lean’s metaprogramming capabilities, and specifically the robust, multimodal visibility which such capabilities grant us into both the proof artifact and the process by which it was constructed. More generally, I think this sense of “visibility” is essential for verification more broadly, and Lean provides such tools through metaprogramming.

Two, I’m betting on the Lean community, which is active, eager (much like Lean’s evaluation semantics!), and, in my estimation of my fellow community members, filled with some amazing people. The metaprogramming capabilities mentioned above are ultimately only as capable as the metaprogrammers who can use them, and I have the good fortune to know some truly capable metaprogrammers in the community. It’s them that I’m betting on.

The statements expressed here (and this bet) are my personal views, and not necessarily those of my employer.

If I win, my winnings will go to the National Immigrant Justice Center.

Mutual conclusion; or, why should you care?

We (Max and Thomas) are posting this wager to draw attention to the problem of Lean soundness bugs and other possible exploits in the face of AI advancement. We want big-lab employees to think carefully about the safety implications of using Lean for RL, in case exploits discovered in the course of training may affect alignment. (We do want big-labs to train models that can formally verify things^[4], as this is load-bearing for several AI safety ideas which we support; we just want them to be careful how they do it!)  We want soundness bugs to start getting Mitre CVEs, and we want FM projects to be sufficiently resourced to triage and fix bugs as they come in (rather than turning them away as uninteresting).

On the Lean formalization side, we must bulletproof ourselves against misformalizations and misinformation. We should start treating formalized definitions with the same suspicion we might treat the introduction of axioms in ordinary mathematical practice. As such, we need widely adopted infrastructure for managing and limiting the trust cost introduced by mathematical definitions and theorem statements in large formalizations, human or AI.

We also want to encourage folks with funding to pay for the humans who work hard, every day, to develop the Lean kernel at the Lean FRO; the humans in the community who are working to create a verified Lean kernel; and the humans on the mathematical side who push forward our understanding of the type theory at the bottom of all this—and likewise for other tools such as Rocq, ACL2, etc. These groups are doing thankless and incredibly important work, and if the fate of your multi-million-dollar training run rests at least partially on their backs, you should be supporting them.

Hopefully our small wager (not small for us!) will help drive conversation vis-a-vis all of the above.

1. ^{^}

   Just a few months ago, this seemed impossible.

2. ^{^}

   To be announced shortly.

3. ^{^}

   (if you, dear reader, know the answer to this, I’d love if you’d share in the comments below)

4. ^{^}

   Well, we both feel this way about proving software correct; doing pure mathematics is a much more nuanced subject where we think there’s a lot more to say about the role of AI, the future of academia, and so forth, and we don’t have time or space to get into that today.