The AI Safety Formalization Atlas: a machine-checked memory for AI safety mathematics

Abstract

Lean's kernel certifies that a proof proves its statement. The kernel cannot tell whether that statement is the claim its author intended. We call a correct proof of a statement other than the intended one a specification failure. We present the AI Safety Formalization Atlas (AISFA), an open Lean 4 library and ledger that together form a shared record of AI safety mathematics. The library holds about 176,000 lines of Lean, all checked by Lean's kernel. AI coding agents wrote all of the Atlas's own Lean, and people check the critical points, such as the bridges that read a result as a claim about AI systems. The ledger's 144 rows record what the Lean means and where each result came from. Every Lean statement that transcribes a printed claim is graded against print, the wording of its published source. Unproved inputs are named hypotheses, never axioms. A theorem about a model owes a witness, an example that satisfies its hypotheses. We graded the Lean renderings of 315 printed statements against print. Three printed claims of Wolpert (2018) fail under this grading. Machine-checked countermodels refute an entropy bound and the claim that another bound is attained. The third claim cannot be carried out as printed, because its construction leaves the class of targets that the paper allows. We used the Atlas as a public verifier for nine solutions that the community submitted to open problems of Math for AI Safety. Four are checked, three are partial and two are conditional.