Testing can prove an AI system is unsafe. It can never prove one is safe.
Proof can. This is a library of proofs about what AI systems can and cannot do — written in Lean, so a computer checks every step.
AI systems are getting more capable faster than anyone is coming to understand them, and they are being released anyway. The decisions about what is safe to build are being made right now, on evidence that can only ever point one way.
Evaluations, red-teaming and incident reports find failures. They cannot show there are none left. The more a system can do, the more ways it can behave, so the share of behaviour any test covers gets smaller exactly as the stakes get higher. A proof is the only kind of evidence that covers every case at once.
The claims that carry the most weight in AI safety are already mathematical ones. That a property cannot be checked automatically. That conflicting values cannot be combined fairly. That you cannot always tell what a system wants from what it does. These get argued in prose, rebuilt from scratch each time, worded a little differently each time — so arguments that could be settled run for years instead.
Writing them down properly used to take a specialist months. It no longer does: language models draft the proof, and Lean's kernel decides whether it holds. The kernel does not care who wrote it, so nothing has to be taken on trust. AI is the subject here, the instrument, and the deadline at once.
A proof settles whether an argument is valid. Whether it is the right argument — whether the mathematics matches the system in front of you — is still a human judgement. That question is worth arguing about. The mathematics underneath it is not, and this library is how it stops being.
A Lean 4 library plus a ledger. The library holds definitions, theorems and counterexamples, all kernel-checked with no sorry. The ledger records where each result came from, which external formalizations exist for it, under which licenses, at which pinned revisions, and what a given development does and does not cover.
Two things it is deliberately not. It is not a certification tool — a theorem is not a safety case, and applying one to a real system takes a separately reviewed interpretation step. And it is not a survey: everything here compiles.
Scope is stated per result rather than assumed. Several entries are reusable cores drawn from larger papers, with the remaining material recorded as an open gap instead of quietly absorbed. That bookkeeping is the reason the library can be cited without a reader having to guess how much of a paper a file really contains.
Downstream proofs need only the root import, but start from a domain facade — each one opens with a table of its primary declarations and an explicit list of what it does not claim.
import AISafetyAtlas.Control -- Ashby's variety bounds, Touchette–Lloyd's information limits import AISafetyAtlas.Logic -- Gödel I/II, Tarski, Löb, Chaitin import AISafetyAtlas.Computability -- Rice, halting import AISafetyAtlas.Learning -- no-free-lunch cores import AISafetyAtlas.Learning.Sharp -- when a no-free-lunch argument applies at all import AISafetyAtlas.SocialChoice -- Arrow, Gibbard–Satterthwaite import AISafetyAtlas.Preference -- planner/reward unidentifiability import AISafetyAtlas.Knowledge -- what an observer can recover about a system import AISafetyAtlas.SelfAwareness -- limits on complete self-monitoring import AISafetyAtlas.Wireheading -- reward channels, self-modification import AISafetyAtlas.Compositional -- hyperproperties, contracts, networks import AISafetyAtlas.InformationTheory.Fano -- peers, no facade: import the one needed import AISafetyAtlas.InformationTheory.DataProcessing
One import does not always mean the whole domain. Wireheading, Compositional and joint observation re-export theirs; Knowledge and Preference are kernels whose specializations are imported individually, so that a kernel can still state what it excludes. Control aggregates nine modules; InformationTheory has no parent at all, because each of its modules is one result and none is built on the others. The root module lists the contract for every parent. Two different things are called control here: Inference has Wolpert's, a device controlling another device, and Control has a regulator against a disturbance. No theorem identifies them.
Everything rebuilds under documented commands, and the axioms each headline theorem depends on are checked mechanically — bounded to the three standard ones, and several results use none at all.
The bottleneck is not Lean. Stating a safety property precisely enough to be checkable is the hard part, and it does not require knowing what a proof assistant is. Pointers to results worth cataloguing, corrections, and open questions with no proof all have somewhere to go.
What is in the library today, and what each one is good for. Impossibility results dominate because that is where the field's load-bearing claims are — but possibility results count too, and the last group holds two of them. The summaries are a plain-language guide; follow each result for its exact statement and scope.
| A verified behaviour, run Fisher, Dennis & Webster | A robot that passes its check keeps passing it while it runs. Use: Turning a verification verdict into a claim about what an agent does. |
| Having the source is not the bottleneck Atlas-side bridge over Rice's theorem as carried by this repository's computability layer; the question is Open Problem 55 of Reuel, Bucknall et al., TMLR 04/2025. The result bounds only the behavioural half of that question and is not evidence about the structural half, which is the same paper's Open Problems 21 and 22 | Hand a checker the complete source of a program and ask two questions about it. Ask what the program *does* -- whether it computes a particular function -- and no checking procedure can always answer correctly, however much of the source it has. Ask what the program *is* -- whether it is this exact source file -- and a checker answers at once. Same source, same access, opposite outcomes. So the classical impossibility result is about questions that depend only on behaviour; it is not a statement that inspecting a system is futile, and in particular it says nothing at all about questions concerning a system's internal structure. Use: When a classical undecidability result is cited to argue that inspecting or auditing a system cannot work, and when deciding whether a proposed property is behavioural or structural. |
| Online robot verification van Leeuwen & Wiedermann | No monitor can guarantee a robot with unlimited memory always behaves. Use: Watching systems that act in the world. |
| Rice's theorem Rice | You cannot build a tool that reads any code and tells you what it does. Use: Why no tool can vet arbitrary AI code. |
| Some things cannot be checked one run at a time Atlas-side bridge: the mathematics is this repository's hyperproperty layer; the questions are Open Problems 18 and 19 of Reuel, Bucknall et al., TMLR 04/2025, which the theorems bound and do not answer | An evaluation that scores every run a system can produce, with a score that decides acceptability, settles every requirement of the form 'each run must be acceptable'. It cannot settle requirements about the collection of runs taken together -- such as 'the system behaves in only one way' -- as soon as it records a summary rather than the whole run, because two different systems then produce exactly the same record. Running it more times does not help: the missing information was never in the record. Use: When an evaluation result is offered as evidence that a system is safe, and when deciding whether a gap in an evaluation is answered by more testing or needs a different instrument. |
| The halting problem Turing; Church | You cannot build a tool that tells you if a program will ever stop. Use: The root of most impossibilities here. |
| The harming problem Alfonseca et al. | No procedure decides exactly, for every program and input, whether it will perform an effect that can be appended to an arbitrary computation -- the kind of effect you are trying to prevent. Use: Deciding what a safety check before deployment can promise. |
| Chaitin incompleteness Chaitin | A system cannot prove that anything is much more complex than itself. Use: Limits on what a system can prove about complexity. |
| Gödel incompleteness I & II Gödel | Some truths cannot be proved. A system cannot even prove it is consistent. Use: Systems asked to verify themselves. |
| Lawvere fixed point Lawvere; Yanofsky's uniform treatment | One argument underlies Cantor, Gödel, Tarski and Rice. Use: Telling apart arguments that are the same from ones that only rhyme. |
| Löb's theorem Löb | Saying “if I prove it, it is true” already proves it. Use: Why an agent cannot simply trust its own reasoning. |
| Physical knowledge is not omniscience Wolpert | Knowing premises can make a conclusion true without making it known. Use: Separating truthful reasoning from logical omniscience in embedded devices. |
| Physical-knowledge boundary cases Atlas audit of Wolpert 2018 | Two tempting epistemic closure claims fail in the source's own device model. Use: Executable countermodels prevent false logical-omniscience and positive-introspection claims from entering the API. |
| Tarski undefinability Tarski | A language cannot define truth for its own sentences. Use: Systems that score their own output. |
| A filing is only as good as what it leaves out Atlas-side bridge: the mathematics is this repository's joint-observation layer; the question is Open Problem 60 of Reuel, Bucknall et al., TMLR 04/2025, which the theorems bound and do not answer | When every party in a supply chain files a declaration, the declarations together can settle any question the underlying evidence settles -- but only if each declaration keeps what the question needs. If two different situations produce identical filings from everyone, no registry built from those filings can tell them apart, and adding more parties to the chain helps only if some new party's filing tells them apart; parties whose filings also agree add nothing. The fix is a more informative filing, not a longer chain. Use: When an audit registry or disclosure regime is proposed as end-to-end assurance, and when deciding whether a gap is answered by enrolling more parties or by changing what each party must disclose. |
| A node's view decides its state after Angluin; a shared-API formulation, no novelty claimed | In an anonymous network, how far a node can see decides what state it ends up in. Use: The positive side of the same law: when a limited observation is nonetheless enough. |
| Ambiguity counting Workbench infrastructure | Counts the answers an observation leaves open. Use: Ruling out an observability claim by counting. |
| Ambiguity over a window Workbench infrastructure | Asking about more of a system can only leave more possibilities open. Use: Bounding how far a monitor's picture can drift. |
| An audit tells you about the thing it audited Atlas-side bridge: the mathematics is this repository's temporal knowability layer; the question is Open Problem 63 of Reuel, Bucknall et al., TMLR 04/2025, which the theorem bounds and does not answer | An audit gathers evidence at one moment about a system that keeps changing. It settles what the system was when it was examined, and on its own need not determine what is running now -- not because auditors are careless, but because the same audit report is consistent with the audited version still running and with a different one having replaced it. Auditing again later recovers more about the past; that alone does not settle the present, and nothing here excludes later records that do. Use: When an audit or evaluation result is offered as evidence about a deployed system, and when deciding whether to answer that by auditing more often or by requiring the deployment to attest to what it is running. |
| Approximate inference escapes the exact limit Wolpert | Two observers that cannot each infer the other exactly can each infer the other to any accuracy short of certainty; an observer that can reproduce another observer inherits none of its accuracy; and a question with at least three answers always has some observer that answers it. Use: Fixes what the observation limits do and do not rule out once observation is noisy, gives the cardinality condition under which an inferring device is guaranteed to exist, and bounds how low inference accuracy can go. |
| Behavior need not reveal the model Atlas, over a construction filed against MAIS-O23 | Three different causal pictures of the same two variables can produce exactly the same behavioral transform on every task in a family, including every rational randomized mixture of interventions, while satisfying every explicit non-degeneracy condition the setting imposes. Lean now checks the forward step from equal transforms to one shared zero-regret policy family; the source's converse oracle reconstruction is not claimed. Watching what an agent does can leave its picture of the world undetermined. Use: Checking whether a proposed method for reading a world model off behavior has ruled out the cancellations that make behavior blind, or only assumed them away. |
| Behaviour does not pin down a causal model a shared-API formulation over the atlas's own causal decision layer, no novelty claimed | If two causal models act the same under every test, nothing that tells them apart can be read off their behaviour. Use: When behaviour is the only evidence about a causal structure. |
| Causal influence diagrams and material observations Atlas transcription of Everitt et al., AAAI 2021, Definitions 1-5 | A causal influence diagram with decision and utility vertices, structural equations with exogenous noise, policies as structural functions, and the observations whose removal costs the agent utility. Use: Stating Everitt et al.'s setup - submodels, policies, expected utility in the induced structural model, and materiality - without claiming any incentive concept or graphical criterion. |
| Coalition coverage Workbench infrastructure | A group sees only what its members share. Processing cannot recover the rest. Use: Designing oversight that can actually work. |
| Data processing Cover & Thomas | No amount of processing a measurement adds information about what was measured. Use: Why a pipeline cannot recover what its first stage discarded. |
| Decision tasks as influence diagrams Richens and Everitt, ICLR 2024, Section 2.2 and Appendix A.1 | A decision task written as a causal influence diagram with the decision and the utility as vertices of the network, together with expected utility, optimality and regret at the source's own quantifiers, and the unmediated-task assumption with the graph consequence the source draws from it. Use: Stating a single-decision single-utility decision task where the decision node's table is the policy, and deriving that under an unmediated task the decision's only route to the utility is the direct edge. |
| Embedded self-measurement Breuer | A sensor inside a system cannot exactly measure every state of that system. Use: The measurement version of the limit. |
| Fano's inequality Fano; Cover & Thomas | Guess wrong often enough and the thing you are guessing about stays uncertain — by a fixed amount you can compute. Use: Turning an error rate into a hard floor on what is still unknown. |
| Finite evidence decides a safety verdict after Clarkson & Schneider; a shared-API formulation, no novelty claimed | If a safety check reads only finitely much of a run, two runs that look alike must get the same verdict. Use: When a monitor sees only finite evidence. |
| Four conceptions of freedom List & Valentini; Carter & Shnayderman | Whether you are free can depend on other possible worlds, and on whether the obstacle was permitted - two independent choices, four answers. Use: When a claim about autonomy has to say which notion of freedom it is using. |
| How many incidents were there? Atlas-side bridge: the mathematics is this repository's knowability kernel; the individuation question is Sidhu et al., arXiv 2026, which the theorem bounds and does not answer | An incident regime publishes a count. That number is computed from what deployments file, and where two deployments file identically while differing in what actually happened, no counting rule whatever recovers the difference -- so the figure measures the filing schema rather than the incidents. It can still be compared with other figures and with targets; what the comparison does not show is a fact about incidents: a count that meets a target expressed in incidents does not show that the incidents meet it, and a difference across regimes or across a schema change may reflect the schemas rather than the incidents. Where the filing does determine the count, a rule exists -- that is the definition unfolded, and it does not say any real form determines the count; under a collision no counting rule is the repair, which is what the obstruction makes precise by quantifying over every rule. Use: When an incident count is published, compared across jurisdictions or time, or written into a target; and when designing what an incident report has to contain. |
| Knowability and inference devices Workbench infrastructure | A device blind to the same distinction in every configuration it can reach cannot answer the question, and cannot know the answer either. Use: Lets an oversight file apply a device impossibility without restating it, and says exactly when the two notions of recoverability do not connect. |
| Knowability kernel Workbench infrastructure | You can tell things apart only if they look different. Use: The shared core behind the observation results. |
| Limited self-awareness Brcic & Yampolskiy | A bounded agent cannot completely monitor every recursively composable internal process under strict positive awareness cost. Use: The process-compositional version of a self-awareness limit; cycles are allowed. |
| More access answers more questions, and no cleverness substitutes for it Atlas-side bridge: the mathematics is this repository's knowability kernel; the question is Open Problem 37 of Reuel, Bucknall et al., TMLR 04/2025, which the theorems answer inside a model of access and do not answer for any named real access level | Ways of examining an AI system can be ranked by how much they reveal: reading the system itself reveals at least as much as seeing its scores, which reveals at least as much as seeing only its answers. Anything establishable from a weaker form of examination is establishable from a stronger one. The other direction is the useful part: if a question cannot be answered from what a form of access reveals, then no analysis of that evidence answers it either -- not more queries, not adaptive probing, not any statistic -- because the missing information was never collected. A worked case shows all three levels genuinely differ, with a property that no amount of testing can detect and that reading the system settles at once. Use: When deciding what level of access an audit or evaluation requires, and when someone proposes to substitute a more sophisticated testing methodology for a higher level of access. |
| No general behavioural safety checker Melo, Maximo, Soma & Castro; proved via Rice's theorem | No program can read another program and always say correctly whether its input/output behaviour is acceptable. Use: When a proposal assumes an automatic checker for arbitrary models. |
| Pearl causal Bayesian networks as a condition on an interventional family | Pearl's causal Bayesian network, stated as a condition on a whole family of interventional distributions rather than on one distribution, with the truncated-product formula derived from it. Use: Deciding whether a family of interventional distributions is generated by a single causal graph, and obtaining the truncated product when it is. |
| Physical knowledge Wolpert | Knowing a fact requires more than producing the right bit: one selected configuration per alternative must answer correctly, and the claimed case must actually occur in context. Use: A precise device-level account of knowledge, truthfulness and an unavoidable unknown target. |
| Physical limits on inference Wolpert | No device inside a system can answer every question about that system, no two distinguishable devices can each infer the other, and no two devices can each emulate the other. Use: Holds for any observation, prediction or recollection device, whatever the physical laws; control inherits every limit. |
| Power in a game form Peleg; the mandate layer is atlas-side interpretation | What a group can guarantee no matter what everyone else does, and which properties of that come for free. Use: When asking whether delegating a decision costs the principal anything it could previously guarantee. |
| Regret and identified-set radius Atlas infrastructure over MAIS-A2 objects | A policy's utility, regret tolerance, and shared behavior define an identified set of causal models; equal transforms are proved to supply one shared zero-regret policy family, and the residual model error is a radius question. Use: Stating interventional value, printed max-regret within the policy type over an ordered value field, of which the printed real case is an instance, and an identified-set relation, without claiming the O27/O28/O34(b) objects. |
| Reward is not knowable from policy Armstrong & Mindermann; a shared-API formulation of the row above, no novelty claimed | Behaviour alone does not pin down the reward: no single rule turns every policy back into the goal that produced it. Use: When behaviour is the only evidence about a goal. |
| Self-modelling Workbench infrastructure | A system can fully know itself only if there is nothing else to know. Use: The precise sense in which nothing can fully model itself. |
| Time-indexed knowability shadows filtration theory; no novelty claimed for time indexing | You can learn what the state was. Not always what it is now. Use: Stating self-knowledge limits correctly. |
| Unknowability has an error rate Atlas, over Fano; Cover & Thomas | If what you want to know is not fixed by what you can see, no procedure reading your observations gets it right more often than a computable floor allows. Use: Turning "this monitor cannot distinguish those cases" into a rate no amount of cleverness downstream improves on. |
| When a proxy reward can disagree Skalse, Howe, Krasheninnikov & Krueger | Two reward functions are hackable when some change of policy looks like an improvement to one and a loss to the other. Use: When checking whether a proxy objective can be optimized against the objective it stands in for. |
| When self-measurement fails extends Breuer | It fails when something else in the system varies, or the sensor is too small. Use: Applying the limit without assuming what you want to prove. |
| Whole-state self-measurement after Breuer | To know the whole state, you must be able to tell every pair of states apart. Use: The basic version of the limit. |
| You cannot read unaided skill off assisted work Atlas-side bridge: the mathematics is this repository's capability-decomposition layer; the measurement question is from the International AI Safety Report 2026 section 2.3.2, whose own caveat is that this research is nascent and further supporting studies are warranted. Nothing here is evidence that any decline occurred, and no model of how capability changes over time is used | Suppose what a person produces with a tool is their own ability plus whatever the tool contributed. Then watching the finished work tells you nothing reliable about the ability on its own -- and this is not a matter of better metrics: any score, rubric or productivity measure computed from that work reads the same evidence and inherits the same blindness. Two situations can produce identical output while the underlying ability differs sharply, and the output can even rise while the ability falls. Taking the assistance away and testing does settle the question, and it is not a more thorough version of watching the work -- it is a different measurement that nothing else approaches. Use: When deciding whether a deskilling or dependence concern can be monitored through ordinary performance data, and when a withdrawal-based assessment is proposed and its cost questioned. |
| You do not have to know which case you are in Atlas-side interpretation of an unpublished sketch; the sketch's pairwise obstruction is kept as a sufficient condition and its converse is refuted here | A system that cannot tell two situations apart can still act correctly in both -- it only needs one action that is acceptable in each. A fixed rule from what is observed to what is done exists exactly when every group of situations that look alike shares at least one acceptable action, and fails exactly when some such group shares none. Use: When a proposal is rejected because a monitor cannot identify the situation, or accepted because it can: the question is not identification but whether the situations it confuses agree on something safe to do. |
| A checklist everything passes and nothing satisfies Peleg's game-form layer; the catalogue reading is atlas-side interpretation of an unpublished proposal | Scoring requirements one at a time asks only that each has some setting that meets it; two requirements that conflict then both pass, and no single setting meets both. Use: When a system is assessed against a list of capabilities or guarantees evaluated independently. |
| A decision cannot beat the evidence it is given Atlas-side interpretation of an unpublished proposal; the total-variation reading is standard | If several situations look identical and each needs a different response, success is capped by how many situations there are, and flipping a coin does not help; in the two-situation case the cap is set by how far apart the observations are statistically. Use: When setting a success target for a monitor or a controller that sees only part of the situation. |
| A policy's long-run value without a finite world Blackwell's sufficient condition; Lean fixed-point core adapted from danlyng/Econlib | The discounted value of a fixed policy exists and is unique on a state space of any size, once rewards are bounded, and it agrees with the finite-state version wherever both apply. Use: When a decision model has too many states to enumerate and the question is whether its value is still well defined. |
| A skill that is topped up enough never falls below its floor -- and the number you can see does not tell you whether it did Atlas-side interpretation of an unpublished sketch; the recurrence is a selected model and is carried as a hypothesis, not asserted | If a capability fades at a fixed rate and is refreshed by at least a computable amount each period, it stays above a chosen minimum forever. Separately, the output a team produces while being assisted cannot reveal how much of that output would survive if the assistance were withdrawn: output can rise while the surviving capability falls. Use: When deciding how much practice a dependency must be paired with, and when someone offers assisted throughput as evidence that capability has been retained. |
| A system that refuses everything passes a safety audit Peleg's game-form layer; the D8 reading is atlas-side interpretation of an unpublished proposal | Keeping every guarantee you already satisfy is free if you never act; a specification has to ask for two things that cannot both happen before refusal stops being an answer. Use: When an assistant or controller is evaluated against a list of properties it must preserve, and nothing on the list rules out doing nothing. |
| A threshold certifies the cases nobody studied Atlas-side bridge: the mathematics is this repository's extremal-Goodhart layer, itself an atlas-original sharpening of Manheim and Garrabrant (arXiv:1803.04585v4), which numbers no theorem; the question is Open Problem 92 of Reuel, Bucknall et al., TMLR 04/2025, whose first half -- which property indicates risk -- is empirical and is not addressed | Suppose a measurable property of a system is picked as a regulatory target because it tracks risk, and a threshold is set that a system must clear. Suppose further that the threshold is set above anything the studied systems displayed, which is the case where a rule is meant to bind on systems more capable than those anyone has examined. Then every system it certifies falls outside the population where the property's link to risk was actually established. Inside that population the property predicts risk as well as it ever did. Outside it, the same evidence is consistent with the true risk being off by any amount at all, at every certified system. Raising the threshold does not repair this: every higher bar also certifies only systems outside the evidence base. Use: When a measurable property is proposed as a compliance threshold, and when the response to a rule that seems too weak is to demand a higher score rather than to widen the evidence base. |
| A vote with no power, and the fine print on measuring it Atlas-side interpretation of an unpublished proposal; the indices are Shapley-Shubik and Banzhaf, with the classical weights as stated by Pitz and Ferraz (2026), which is cited as a neighbour and not graded | In a voting rule where adding members never loses a vote, two standard power scores are zero for exactly the participants who can never change any outcome -- and a participant holding a third of the nominal weight can be one of them. Drop the monotonicity and a zero score stops meaning powerless, because gains and losses cancel. Use: When a share of votes, seats or weight is being offered as evidence of influence, or when a zero power index is being read as proof that a party is harmless. |
| Allowed, able, and official are three different questions Separation claim from Jones and Sergot (1996), abstract; the four-status norm annotation is atlas-side design | Whether a system may do something, whether it can, and whether the act officially counts are independent: any combination of the three can occur. Recording prohibition separately from permission also keeps 'the rules forbid this' apart from 'the rules say nothing about this', which collapse into each other if permission is stored as a single yes-or-no. Use: When reviewing an authorization or policy check, or when a design stores permissions as one flag per action. |
| An actuator is worth what it can reach Atlas-side interpretation of an unpublished proposal; the entropy machinery is PFR's | How much a system can influence through a deterministic mechanism depends only on how many distinct outcomes that mechanism produces, not on how many settings it has. Use: When sizing an effector, an interface, or any deterministic channel by its actual influence. |
| An unbroken approval trail proves only what the approval rule forbade Atlas-side interpretation of an unpublished proposal; reachability is Mathlib's | Every change being authorized by the rules in force at the time guarantees nothing if those rules allow anything; the chain inherits its force entirely from the rule. Use: When a system, policy, or model can modify its own governing rules and logs each change as approved. |
| Being able to reach any state is not being able to stay at one Atlas-side interpretation of an unpublished proposal, over the atlas's own linear-systems layer | The standard controllability check asks whether every state can be reached with nothing pushing back; holding a state against disturbance is a different condition, about the disturbance and not about the controls. Use: When a controllability or reachability argument is offered as evidence that a system can be kept safe. |
| Believing what you are told is not deciding for yourself Atlas-side interpretation of an unpublished proposal, which states this as a limitation on Rakow's doxastic notion of an autonomous-decisive system; no coverage of either is claimed | A system can always take the best action its beliefs allow and still control nothing, if somebody else writes the beliefs: everything such a system can guarantee already includes every action its message source can install. Use: When an assistant's autonomy is argued from its acting consistently on its own assessment of the situation. |
| Controllability and observability tests Kalman and Hautus; the criteria adapted from AnandGokhale/LeanForControl, the dynamical layer atlas-original | Two matrix tests that say whether a linear system's inputs can reach every state, and whether its outputs pin the state down - and, since 2026-09-20, the differential system they are tests for, with each test proved equivalent to the property it is named for. Use: When a linear model is on the table and the question is whether the state is determined by what is observed, or reachable by what can be driven - either as an algebraic test or as a statement about the runs themselves. |
| Entitled, able, and obeyed are three different things Peleg's game-form layer; the authority reading is atlas-side interpretation of an unpublished proposal, with the authority predicate left undefined on purpose | Who may decide, who can make it happen, and who can block it come apart in every direction, and watching the system behave does not tell you which you are seeing. Use: When an assistant or delegate is judged compliant because every instruction it received was carried out. |
| Getting a message through when others can interfere Peleg's game-form layer; the coding reading is atlas-side interpretation of an unpublished proposal | A component can reliably signal one of several choices exactly when it can drive the visible result into separate regions, one per choice, whatever everyone else does. Use: When asking whether a subsystem can be guaranteed to convey a decision, or guaranteed not to. |
| Having an answer to every move is not having a plan Peleg's game-form layer; the quantifier reading is atlas-side interpretation of an unpublished proposal | A system that can counter each attack separately may have no single setting that counters them all, and two guarantees it makes separately may be impossible together. Use: When a safety case lists properties a system can enforce, without recording which configuration enforces each. |
| How much a belief moved says nothing about who moved it Atlas-side interpretation of an unpublished proposal, whose section 7.4 definition is transcribed and whose compatibility claim is strengthened to a separation | Two systems can change someone's beliefs by exactly the same amount, one using only evidence the person endorsed and one also using a channel they did not; so the size of the change cannot tell them apart. Use: When judging whether an assistant's influence on a user's beliefs was legitimate. |
| How much someone could move you is not how much choice you lost Peleg's game-form layer; the influence reading is atlas-side interpretation of an unpublished proposal | A provider's capacity to change your outcome and your ability to guarantee your own are separate quantities that can both be at their maximum; and looking only at summaries hides influence that is there. Use: When a dependency is assessed by how the provider currently behaves, or by aggregate statistics. |
| Information limits on control Touchette & Lloyd | Feedback helps only as much as the sensor actually measured. Use: Deciding how much monitoring a control loop really needs. |
| Losing the plot one safe step at a time Peleg's game-form layer; the steering reading is atlas-side interpretation of an unpublished definition | Every step keeps what you currently ask for, and the thing you originally asked for is gone by the end. Use: When a delegation is reviewed step by step and each review asks only whether this step is acceptable now. |
| Moving to a new system without losing what you could insist on Peleg's game-form layer; the transfer reading is atlas-side interpretation of an unpublished proposal | A replacement that produces only familiar outputs can still have taken away every choice you had; what has to be checked is per-option, not output-by-output. Use: When a platform migration, a model upgrade, or an export path is argued to be safe because the results look the same. |
| Randomizing is worth something exact Atlas-side interpretation of an unpublished proposal; the minimax theorem is Mathlib's formalization of Sion after Komiya | In a finite two-party contest, committing to one fixed action can be answered and guarantees little, while randomizing guarantees a definite amount that neither side can improve on. Use: When a defender's guarantee is computed over deterministic policies only. |
| Requisite variety Ashby | A controller cannot hold things steadier than its own range of responses allows. Use: Sizing what a safety controller has to be able to do. |
| Rule engines quietly add two rules nobody asked for Divergence measured against Jones and Sergot (1996); the rule format and the authority decomposition are atlas-side | Encoding 'this action counts as that' with an ordinary rule engine adds two properties the legal-theory account deliberately excludes: everything counts as itself, and counting-as chains together. Both are proved here, so the mismatch is caught by the build rather than by a reader. Separately, an action the rules recognize is still not an action anyone is allowed to take. Use: When encoding institutional or organizational rules as derivations, or when a design treats rule-engine output as an authorization decision. |
| Seeing is not steering Atlas, over Ashby | An overseer that can tell every situation apart may still be unable to steer the outcome, and one that can tell nothing apart may be able to. What you can see and what you can do are separate budgets. Use: Checking whether an oversight proposal is short of information, short of levers, or both. |
| The part of a safe region you can actually stay in Atlas-side interpretation of an unpublished proposal; the fixed-point machinery is Mathlib's | Staying inside a safe set forever is possible exactly from the largest part of it that can sustain itself; the rest only looks safe, and getting back in has a budget that behaves like a countdown. Use: When a system has an operational envelope and a supervisor is meant to keep it inside, or to bring it back. |
| Uncontrollability Kalman; the equivalence with the dynamical property after Chen and Desoer, cited by Klamka 1972 | Some systems cannot be driven from where they are to where you want them, whatever inputs you apply, and there is an exact test for which ones. Use: Before claiming a system is steerable: if the test fails, no control law reaches the states it excludes. |
| Unobservability Kalman; the equivalence with the dynamical property after Chen and Desoer, cited by Klamka 1972 | Watching a system's outputs does not always tell you what state it was in, and there is an exact test for when it does. Use: Before claiming a system is monitorable: if the test fails, no amount of watching the outputs recovers the state. |
| Whose move comes first changes the number Peleg's game-form layer; the value layer is atlas-side interpretation of an unpublished proposal | A success probability against opposition is two different quantities depending on who commits first, and only the smaller one is a guarantee you can deploy. Use: When a safety evaluation reports a success rate measured against a fixed adversary or fixed environment. |
| Why the outnumbered side wins Atlas-original reading of a question about one-to-many power; not from any source, and the incentive side of the question is explicitly not addressed | When many parties could together override one system but can only act one at a time, the system keeps control of situations it would lose if they acted together; nobody's authority changed, only the timing. Use: When an oversight arrangement gives many people a veto that they would have to exercise together. |
| You can act correctly on evidence that cannot say who did it Atlas-side interpretation of an unpublished proposal; the factorization criterion is Mathlib's | A channel too coarse to certify responsibility can still be enough to choose a safe action, provided the situations it confuses agree on one. Use: When deciding what to log or monitor, and whether the same data must serve both attribution and control. |
| No free lunch — optimization Wolpert & Macready | Same for search, but only under an exact condition: averaged over a set of objectives that cannot tell one point of the search space from another, every optimizer scores alike — and almost no set of objectives is like that. Use: Checking whether a "no optimizer is better in general" argument applies to the problem at hand at all. |
| No free lunch — supervised learning Wolpert | No learner beats another once you average over all possible tasks. Use: Making “our method generalizes” name its assumption. |
| Corrupt-reward no free lunch, on the source's own grid Everitt, Krakovna, Orseau, Hutter & Legg | With a corruptible reward channel, no policy can be much better than the worst one. Use: Bounding what any agent can achieve when its reward signal can lie. |
| Goal preservation Everitt, Filan, Daswani & Hutter | An agent that can rewrite itself can still keep its original goal. Use: Self-modification arguments. |
| Goal preservation along the trajectory Everitt, Filan, Daswani & Hutter | A self-rewriting agent that plans realistically never trades its goal away, at any step. Use: Self-modification arguments that must run for more than one step. |
| Histories on the shared carrier Ring & Orseau; Turner & Tadepalli | An agent's horizon can be measured in steps it actually took, not in lists nobody produced. Use: Scoring a real run by an agent's own value recursion. |
| Objective factorization Ring & Orseau | An agent can end up caring about what it sees, not about what is real. Use: Exactly when wireheading is optimal. |
| Overoptimization floors the unmentioned Zhuang & Hadfield-Menell | An objective that mentions only some of what you care about drives the rest to the floor. Use: When choosing which attributes to write into a metric an agent will optimize. |
| Preference unidentifiability Armstrong & Mindermann | Behaviour on its own does not pin down what an agent wants. Use: Learning what someone wants from what they do. |
| Retargetable decision-makers Turner & Tadepalli | A decision-maker that can always be retargeted towards the larger set of options will favour it at most of its settings. Use: When arguing that a tendency comes from the shape of an option set rather than from any particular objective. |
| Reward corruption Everitt, Krakovna, Orseau, Hutter & Legg | If the reward can be faked, the agent cannot tell it is being fooled. Use: Reward tampering. |
| Rewardless Markov decision process Turner & Tadepalli | The dynamics of a decision process, carried separately from any reward defined over them. Use: When the reward is not a fixed part of the environment but something a consumer varies. |
| Selection on a proxy after Manheim & Garrabrant | Optimizing a proxy pushes the system into the tail, and into the region where the proxy was never checked against the goal. Use: When a measure fitted on ordinary conditions is about to be used as a target. |
| Self-modification on the shared carrier Everitt et al.; Turner & Tadepalli | An agent that rewrites itself can keep the goal it started with. Use: Checking a self-modification argument against a model where policies actually differ. |
| Unidentifiability at a trajectory Armstrong & Mindermann | When any planner is admissible, watching an agent for any length of time rules out no reward at all. Use: Bounding what behaviour alone can tell you about what an agent wants. |
| Unobservable return Workbench infrastructure | An agent cannot tell how well it is really doing from what it saw. Use: Ties reward tampering to what an agent can know. |
| Value reinforcement learning Everitt & Hutter | An agent told to keep its beliefs consistent stops wanting to fool its own sensor. Use: Designing a reward channel an agent has no reason to corrupt. |
| A network's runs, as a system of traces after Angluin and Clarkson & Schneider; the connecting construction is the atlas's own, no novelty claimed | A network's runs can be handed to the machinery that reasons about whole sets of executions. Use: When a property is about all runs at once, not one run. |
| Arrow's impossibility Arrow | No fair way exists to merge people's rankings into one. Use: Combining values across people or models. |
| Fairness criteria that cannot coexist Kleinberg, Mullainathan & Raghavan | A risk score cannot be calibrated within both groups and equally accurate for both classes unless the groups have the same base rate or every case is already certain. Use: Choosing between fairness criteria for a scoring system, when the groups being scored differ in how often the outcome occurs. |
| Gibbard–Satterthwaite Gibbard; Satterthwaite | Every sensible voting rule can be gamed by lying. Use: Asking people or systems to report preferences honestly. |
| Misaligned embodiment Brcic & Yampolskiy; Angluin for the formalized core | The survey claims cloned agents cannot control each other. Only the symmetry result is proved. Use: The difference between a claim and a proof of it. |
| Playability and its failed converse Pauly; refutation by Goranko, Jamroga & Turrini | Pauly's five conditions describe the power of a game, but they do not pin one down. Use: When a claimed distribution of power has to be checked against an actual game. |
| Symmetry in anonymous networks Angluin | Identical processes in identical surroundings can never pick a leader. Use: Why identical agents cannot coordinate. |
| Truly playable effectivity functions Goranko, Jamroga & Turrini | Not every consistent description of who can force what is the description of an actual game. Use: When checking whether a claimed distribution of power could be realized at all. |
| When a share-out of power cannot settle anywhere Keiding (1985), Definition 3.3; the condition is transcribed, the stability theorems it feeds are not | Some arrangements of who-can-force-what are unstable no matter what anyone wants: whatever outcome is proposed, some group can and will block it. Whether an arrangement has that defect is decided by a pattern in the powers themselves -- a cycle -- with no reference to anybody's preferences. Use: When checking whether a proposed governance arrangement, voting rule or veto structure can ever reach a settled outcome, before asking who prefers what. |
| Attribution impossibility DASH trilemma | No way of scoring which inputs mattered meets all the obvious requirements. Use: Claims made for saliency maps. |
| Hyperproperties and k-safety Clarkson & Schneider | Some properties need several runs at once to check. Use: Leaks and fairness — anything one run cannot reveal. |
| Rectangularity Kushilevitz & Nisan; Fagin | A requirement on the whole sometimes splits into requirements on the parts. Use: When checking components separately is enough. |
| Traces of a policy set Clarkson & Schneider | When a group of agents breaks a security property, a few partial runs show it. Use: Reporting a hyperproperty violation as trajectories rather than as abstract prefixes. |
| Conditional normative reasoning Parent & Benzmüller; Parfit's paradox, Åqvist's system E | A logic of obligation, precise enough for Parfit's argument. Use: Population ethics arguments. |
| Deep versus shallow capacity Cohen, Sharir & Shashua | Deep networks compute things shallow ones need exponential width to match. Use: Capability arguments about architecture, not size. |
| Distributed snapshots Chandy & Lamport | A running system can snapshot itself without pausing. Use: Why “a system cannot know itself” is too strong. |
| Doubly-efficient debate Brown-Cohen, Irving & Piliouras | A weak judge can be argued to the right answer by stronger debaters. Use: Judging work you cannot check yourself. |
| Expected utility representation von Neumann & Morgenstern | Consistent preferences can always be written as a utility function. Use: The assumptions inside “maximizes expected utility”. |
| Gibbard–Satterthwaite (independent proof) Gibbard; Satterthwaite | The same voting result, proved again in another system. Use: Independent confirmation. |
| No free lunch (PAC lower bound) Shalev-Shwartz & Ben-David | A different no-free-lunch theorem from the atlas's: no learner beats a coin flip on every distribution when the sample is small. Use: How much data a guarantee needs — not a second proof of the Wolpert averaging results. |
Nothing matches that. The filter reads the result name, its summary, and the credit line — try a shorter word, or clear the box.
These are proofs from other people and other systems, rebuilt from source at pinned revisions to confirm they still hold — not re-implemented in Lean. They carry no Lean import surface, and they are credited in full below.
People file candidate solutions against the MAIS open problems. This library transcribes them into Lean at the source's own quantifiers and puts them to a kernel. Below is every one it has checked, and what checking found.
Two cautions, because these are other people's results. A verdict here is a machine check against a pinned copy of the submission — it is not peer review, and it does not mean a submission has been accepted upstream, where these problems remain listed as open. And the verdict words are not synonyms: PARTIAL and CONDITIONAL mark rows where what is proved is narrower than what was claimed, or rests on something the submission cites rather than derives. Issue bodies can be edited after the fact, so each row is checked against a recorded hash of the text as read.
| Problem | Verdict | What was submitted, and what checking it found |
|---|---|---|
| MAIS-O70 issue #3 · Sneiderman | CONDITIONAL | A complete solution: the local learning coefficients of reduced-rank regression at every rank stratum, with the residual threshold restated as a discrete minimisation over an integer index. Checked: The rank table is transcribed as o70Pair and machine-checked, but under two propositions the candidate cites rather than derives: the real-Wishart eigenvalue law and the existence of exact local pairs. Both are recorded as frontiers with their own evidence, and NC-011 shows that none of the six baseline formalization corpora supplies the first. The discrete minimisation behind Corollary 1.3 is closed unconditionally, as residualMinCost_eq_argmin. The candidate's own section 13 states that exactness at every radius is not claimed, and the atlas matches that co-countable form rather than strengthening it. |
| MAIS-O34(a) issue #4 · Robby955 | CHECKED | A complete criterion for when the global behavioural fibre is a singleton, on the source's real three-parameter two-variable chart, together with a first-order radius constant, a singular classification, and a graph-threshold program. Checked: The criterion is transcribed at the source's own quantifiers and proved, as maisO34_exactFiberCandidate_holds. Separately the atlas settles the margin-sufficiency subquestion negatively: positive margin alone does not force a singleton fibre. The rest of part (b) — the radius constant, the singular classification, the graph-threshold program — is not transcribed and carries no verdict here. |
| MAIS-O7 issue #5 | CHECKED | A negative resolution: in the scalar instance the rank-zero critical set has local pair (1,1) while the terminal fibre has (1/2,1), reversing the conjectured strict increase. Checked: Confirmed and strengthened, though not in quantifier strength: the note already proves the pair at every point of the terminal rung and states that both infima are attained. o7CounterexampleAtEveryScale makes the two-rung certificate a single unconditional object -- the exact exponent set on each rung, attainment as a proposition, and every positive target. The conjectured increase is false. What was checked is the note's claim, not its argument: the note routes the rank-zero pair through the analytic Morse lemma at signature (2,2) and the atlas proves it by an explicit integral instead, so the note's own step is unverified. A 2026-09-06 audit added the two identifications the certificate rests on -- that its rank-zero rung is MAIS-A7's C_0 and its terminal rung that frame's exact-factorization fibre -- which had been transcriptions no check could see, and the descending-loss step that puts the instance inside print's stated setting. |
| MAIS-O23 issue #6 | PARTIAL | Filed as a full solution pending review: three models on two binary variables sharing a behavioural transform, making the MAIS-O23 consequence explicit across all three graphs. Checked: The construction machine-checks, and the atlas goes past it: a positive-dimensional colliding family rather than a point, a narrower two-graph reading that does not depend on the edgeless model being admissible, and transport to the source's real chart rather than a rational restriction. What is verified is narrower than what is claimed. A collision at one skeleton is a possibility result, not the general question, so the atlas does not endorse the full-solution framing; the printed question is answered separately and graded against the agenda. The issue credits its own construction to MAIS issue #4, and the atlas claims no priority for it. |
| MAIS-O24 issue #7 · kumino | CHECKED | A negative resolution: clauses (a) and (c) of the printed problem cannot both hold, so it has no solution. Checked: The incompatibility holds and is machine-checked. The argument as written had a circular step in its choice of measure, which the atlas repaired before checking rather than reproducing. AISafetyAtlas.Causal.O24Solution is the solution type with the proof obligations as fields, and it is empty. |
| MAIS-O31 issue #8 · kumino | STATED_ONLY | A complete solution: four affine diagnostics and a generic chamber classification for one intervention in a binary chain. Checked: Transcribed at the issue's own quantifiers — every threshold in the open unit interval, all four binary local interventions, literal coordinate equality, and the issue's own scope exclusions as the chamber disjunct — and it is not proved. The embedding into the printed margin class is proved in both directions, so the statement is not left semantically detached. The atlas separately refutes the printed heuristic's claim that the endpoint marginal is recoverable, on an explicit box of Lebesgue measure 1/500. |
| MAIS-O33 issue #9 · kumino | CHECKED | A negative resolution: the persistent-corruption threshold is zero. Checked: The submitted value is confirmed, with a caveat the ledger states rather than hides. The upper half is the proved content; the lower half follows from the sign clause together with the supremum of the empty set being zero, not from a proof that the printed zero endpoint is tolerable, and the graded correct answer is the baseline-relative form. An independent audit of the note found no error. The issue reports that its mathematics was generated by an AI system with no human referee review claimed. |
| MAIS-O77 issue #12 | PARTIAL | A complete solution to both clauses: the local pair at every exact factorization together with the minimal stratum, and the pair at every point of every nonterminal critical set. Checked: Part (b) is proved unconditionally at print's own quantifiers, as o77AllSaddlesHavePairOne_holds, following the candidate's five printed steps rather than substituting a shortcut; two results it needs — the splitting of its equation (9) and its Lemma 2 — are absent from the Mathlib revision pinned here and were built here; NC-012 is that search, and it covers Mathlib alone, so it is not a claim about every formalization corpus. Part (a) is verified only under the eigenvalue-law frontier inherited from MAIS issue #3; that covers its minimal stratum too, checked at the germs rather than against the table. Four defects surfaced while checking, all of them the atlas's own -- each a statement that compiled, was axiom-clean, and was about something weaker than print. None was a defect in the submission; no error was found in it. The complete-solution claim is therefore not verified. The note's argument is followed, not replaced. Its equation (9) already writes the generalized splitting -- L - L(w) = Q_alpha(xi) + g(zeta) with g(0) = 0 and no nondegeneracy asked of g -- which is a Gromoll-Meyer splitting, and that is what was built. Only the name it gives the tool, the analytic Morse splitting lemma, is loose. Two departures are worth stating: the atlas proves the splitting C-infinity rather than analytic, which is all the note's Lemma 2 consumes, and loss_quartic_on_degenerateNull rules out a Morse-Bott normal form, which (9) does not claim and does not need. A 2026-09-06 audit closed the remaining prose step in part (a) by proving that the discrete minimisation the atlas computes with is the note's printed four-case closed formula, and pinned the note's own ten check-table values. |
| MAIS-O38 issue #30 · 26david26 | CHECKED | A complete solution in two theorems: that a polynomial number of fixed codes depending only on the dimension and the sparsity suffice below the sparsity bound, and a boundary theorem above it. Checked: The main claim is transcribed and proved, and resolves the graded row at every non-degenerate dimension; its codes being independent of the ambient dimension is one axis on which it is stronger than the claim being graded. The boundary theorem is proved here independently and without one of its hypotheses. The atlas has posted this machine-check on the issue itself. The issue reports that its mathematics was produced and checked entirely by AI systems with no human verification. |
Row by row, with the Lean declaration each submission was transcribed into and the hash it was read at: MAIS submitted solutions.
The library is one node in a wider set of curated collections. These are the directories it is catalogued against — several reached through the first, which indexes the rest.
| Directory | What it collects, and why it is here |
|---|---|
| Math for AI Safety | A living index of research directions for mathematicians entering AI safety, pointing at the collections below. The closest thing to a map of where mathematical work in this field is being organised. |
| The Alignment Project UK AI Security Institute | Eleven priority research areas, each broken into subproblems in prose. The agenda closest to this library's subject matter, and the one most likely to name a problem a formal result could sharpen. |
| MAIS open problems | Ninety-two individually numbered open problems in AI-safety mathematics. Numbered identifiers make it the one collection a formal library can be mapped against precisely, problem by problem — the one already underway, in this library's own conjecture ledger: sixteen MAIS-linked records checked against pinned sources, covering thirteen printed problems of the MAIS agendas — nine in A2, one in A3, one in A6 and two in A7 — with more than one record where a problem's clauses are graded separately, or where a submitted candidate answer is graded beside the printed question. Ten are conjectures, eight have linked Lean proofs; the other two remain open. The rest are determine-problem specifications. Six further A2 problems the atlas cannot state at all carry no ledger row and are recorded against their source instead, so the ledger holds only records with Lean. The ledger also contains one non-MAIS, atlas-original question about Wolpert 2008, labelled as such. |
| Timaeus projects | Project ideas in developmental interpretability and singular learning theory — the statistical-physics-flavoured end of the field, and since the MAIS-O70 work the collection this library overlaps most directly. |
| Iliad ecosystem | Groups working on interpretability and theoretical modelling of learned systems. Useful for finding who is working on a problem rather than which problems exist. |
| Impossibility Results in AI: A Survey ACM Computing Surveys, 2023 | The inventory of impossibility results this library is organised around, and the reason it exists: a survey that catalogues claims is the natural starting point for a library that checks them. |
Mapping the individual numbered problems in these collections to machine-checked results is underway for MAIS's open problems; the rest are not yet mapped.
Every external formalization this library depends on or reproduces is recorded with its license and an immutable revision. Reproduced means the proof was rebuilt from source, not that a link was cited.
| Project | System | License |
|---|---|---|
| mathlib4 | Lean | Apache-2.0 |
| FormalizedFormalLogic · Foundation | Lean | Apache-2.0 |
| SocialChoiceLean | Lean | MIT |
| ChihChengLiang · arrow | Lean | Apache-2.0 |
| kolmogorov-complexity-lean | Lean | Apache-2.0 |
| dash-impossibility-lean | Lean | Apache-2.0 |
| google-deepmind · debate | Lean | Apache-2.0 |
| vNM-Theorem-pub | Lean | Apache-2.0 |
| tcslib | Lean | Apache-2.0 |
| AFP · Chandy_Lamport | Isabelle/HOL | BSD-3-Clause |
| AFP · ArrowImpossibilityGS | Isabelle/HOL | BSD-3-Clause |
| AFP · No_Free_Lunch_ML | Isabelle/HOL | BSD-3-Clause |
| AFP · Recursion-Theory-I | Isabelle/HOL | BSD-3-Clause |
| AFP · Deep_Learning | Isabelle/HOL | BSD-3-Clause |
| AFP · CondNormReasHOL | Isabelle/HOL | BSD-3-Clause |
| exploring-robust-property-preservation | Rocq/Coq | Apache-2.0 |