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.
| 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. |
| 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. |
| 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 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. |
| 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. |
| 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. |
| 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. |
| 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 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. |
| 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. |
| 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. |
| 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. |
| 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. |
| Goal preservation Everitt, Filan, Daswani & Hutter | An agent that can rewrite itself can still keep its original goal. Use: Self-modification arguments. |
| 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. |
| 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. |
| Reward corruption Everitt, Krakovna, Orseau, Hutter & Legg | If the reward can be faked, the agent cannot tell it is being fooled. Use: Reward tampering. |
| 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. |
| 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. |
| Symmetry in anonymous networks Angluin | Identical processes in identical surroundings can never pick a leader. Use: Why identical agents cannot coordinate. |
| 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. |
| 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 |