Paper 2026/2441

Nobody Will Read the Lean: A Case for High-Level Cryptographic Languages

Abstract

In September 2026, an AI produced a Lean proof of Fermat's Last Theorem in eleven days, and AI provers have started on cryptography. Within a few years, an AI may hand you a machine-checked proof that Signal is secure. You won't need to read it, because Lean will have checked every step. What Lean can't check is whether the theorem says what you think it says. That depends on its definitions, which the AI will also have written at length for that one proof. This already happens. A Lean library's security theorem for Schnorr signatures passed the checker, yet as written it held for every adversary and so promised nothing. When proofs are cheap, the scarce resource is a person who can read what was proved. I argue that we should build high-level cryptographic languages for that person. A protocol's owners should write its model themselves, short enough for one or two people to read. Every claim the language makes should rest on a checked theorem. And definitions of protocol goals such as forward secrecy should be built in: a small set, versioned and agreed in public the way we agree on AES, so that a property's name means the same thing in every report. Today it may not: on a one-page Verifpal model, two of five verdicts would flip under other standard definitions, with neither answer wrong. Agreeing on definitions will take years of public argument that better provers can't shorten, so we should start now.