One area, debate and scalable oversight, now works as a discovery engine.
What the atlas is
A map of AI-safety research that you can check. Every record quotes its source exactly, every link says why it exists, and nothing counts until it passes checks built to catch planted mistakes.
245pinned sourcesPapers, Lean and Mathlib, Metamath, each fixed to one version
1,750recordsEach a claim, definition, theorem or result, quoted with its page and lines
5,821typed linksBuilds on, disputes, proof uses; each with the reason it exists
539/542planted mistakes caughtTwo blind AI checks; Lean's kernel for proofs; a person's sign-off on a few
3ways inThis site's views, llms.txt for AI agents, and the raw data
Every record, as a dot
All 1,750 records, grouped by what they link to. Click a dot to read its quote, source and links. Open it full screen →
What it can do as a tool
Check a result before you rely on itIts exact source line, its conditions, how strong its evidence is, and any problem found in it.
See what is still openOpen questions ranked by the safety-case step they would move.
Trace what a result assumes30 assumption families, and where the safety case relies on each.
Put AI agents to work on itAgents read the same map and can take research roles, from reader to prover (below).
One way to use it: from a question to an experiment
Everything is downloadable: the public view with every record and link, and its hash manifest. Code is Apache-2.0 and data CC BY 4.0.
What's in it
1,750 records and 5,821 links, built from 245 pinned sources. Most of the depth sits in one area.
997formal maths: Lean and Metamath theorems, definitions and their proof links657debate and scalable oversight, read in full from 42 papers9622 other AI-safety topics, mostly sampled from abstracts
Sources quoted
Full text read
Open questions mapped
Gaps attacked
Two AI checks
Person reviewed
Debate & scalable oversight42 papers
22 other topics37 papers, mostly abstracts
Formal mathsLean, Mathlib, Metamath
Half-filled means part of it. A few formal records and links carry a person's sign-off; none of the debate pilot's results do yet.
What it found
The four results that matter most from the debate pilot. All are AI drafts that passed two blind AI checks; none is confirmed by an expert.
DebateTwo AI systems argue opposite answers and a judge, a person or a weaker AI, decides. The hope: honesty wins, so a weak judge can oversee a strong AI.
Safety caseA structured argument, broken into steps, that a system is safe enough to deploy. Every step needs evidence.
LeanA programming language for maths. A computer checks every step of a proof written in it.
The debate safety case
2 of 45 steps have checked support
Buhl et al. 2025 sketched a safety case for debate in 45 steps: the top claim, 22 supporting claims, 4 assumptions, 12 ways the argument could fail, 4 open problems and 2 kinds of evidence it still needs. We matched every step against the results in the 42 papers.
supported 2
one strong or two moderate results back it, and none undermines it
contested 1
results point both ways
weak 28
only weak or indirect results bear on it
none 14
nothing in the papers bears on it
Supported: “Efficient equilibrium debaters exist” and “Protocol avoids obfuscated arguments”, both backed by Brown-Cohen et al. 2025. Contested: “Human judges have bounded systematic error”.
Problems in the papers
52 problems in 5 papers' theorems
error 9gap 22ambiguity 21
A theorem is a statement with a proof; papers number them, like Theorem 2 or Lemma 3. We restated the theorems of 5 papers in Lean, which forces every condition into the open. An error means something printed is wrong; a gap, a proof step that is skipped; an ambiguity, a statement that can be read two ways.
Debate beats consultancy in 51 of 56 matched comparisons
In consultancy a single AI argues for one assigned answer; in debate two argue both sides. Each dot is one matched comparison on the same task: how many points more often the judge picked the right answer with debate.
other 4 papersKenton et al. 2024 (33)points of judge accuracy
The median gain is +8.4 points across 5 papers, but 33 of the 56 comparisons come from one paper and 45 use LLM judges.
Authors' open questions
27 of 33 moved forward
partly answered 12narrowed 15still open 6
Questions the papers' authors left open, worked once by the pilot. Narrowed means a smaller version is now settled and what remains is stated; partly answered means later papers settle part of it.
6 questions now have a Lean proof of a narrowed version, and 5 come with a suggested experiment. None is fully answered.
The finding that cuts across all four: the five assumptions the papers rely on most appear in no step of the safety case. The safety case leans on "training reaches equilibrium" (15 steps), which only 6 results address.
How useful is it? The report card so far
Measured on the debate pilot. Solid bars are measured; empty ones are tests not yet passed or not yet run.
Measured
Open questions it can answer from its records45 judged by two AI checks, 7 by a person19 fully, 19 partly, of 52
Quotes that match their PDF word for wordall, in 42 papers
Planted mistakes its checks caught539 of 542
Records a good answer needs that search finds63%
Debate results graded by their evidence152 rest on a single settingall 248
Not yet shown
Errors an expert has confirmed0 of 9
Discoveries a person has reviewed0 of 96
Time it saves a researchertest not run
People outside this project using itnone yet
Today it is most useful as a map of what is actually established about debate, and a ranked to-do list of what is not.
A research team of AI agents, on one shared map
The work splits into roles. Every role reads the same atlas and writes back only what passes the checks, so one agent's result becomes the next one's starting point.
Reader
Reads each paper line by line and quotes it exactly.
42 papers, 657 records
Theory discoverer
Finds the assumptions results share, and combines known results into new ones.
30 assumption families, 11 results derived
Definer
Lines up each paper's definition of a term and says where they differ.
59 definitions quoted, not yet compared
Prover
Proves narrowed versions of open questions in Lean.
6 questions narrowed with a Lean proof
Experimenter
Designs, and later runs, the experiment an empirical question needs.
5 experiments designed, none run yet
Auditor
Restates published theorems in Lean to find what is wrong or missing.
52 problems found in 5 papers
Checker
Re-reads every claim against its source, blind, twice.
539 of 542 planted mistakes caught
Explainer
Writes a plain account and a quick self-test for each key result.
not started
The atlasOne shared map. Each role reads it and writes back only checked work.
ran in the pilotpartlynot yet
In the pilot these roles were played once, on debate, by this project's own agents. Outside agents can read the map today through llms.txt; taking a role and writing back is the next step.
From an open question to a finished result
The atlas can carry a project from start to finish: pick the question, name what blocks it, do the work, check it, report it, then move to the next blocker. The pilot ran this loop once.
1Choose
Open questions ranked by the safety-case step they would move.
Then the next blocker, on the next question. Not automatic yet: the loop runs on its own once a person has reviewed the pilot's results, and from then on people review only what changes the safety case.
livepartly, or run oncenot yet
The best next steps
Credibility first, because it multiplies everything else. A new area built on unconfirmed checks would inherit the same doubt.
1
Get the finds confirmed
Experts check the 9 errors from short notes: the claim, the Lean counterexample, a suggested fix. People review only a small core of debate statements, each shown beside a blind plain-maths read-back of its Lean version; AI checks cover the rest. That turns the first results into findings people can cite.
2
Measure usefulness automatically
An agent answers the 52 authors' questions with and without the atlas. We report accuracy, sources found and time taken. No people needed, and it gives the first real answer to "does this help?".
3
Make the results understandable
Understanding cards for the results the safety case leans on, and a blocker label on every open question so each one gets the right kind of agent.
4
Run the first stress test
Loosen "training reaches equilibrium" and find which of the 15 safety-case steps that rest on it still hold. Only 6 results address it today.
5
Then open the next area
Make debate a living area (below), and run the same pipeline on AI control and monitoring.
Debate and scalable oversight: from map to engine
Five stages that would make the atlas the place where the state of debate research is kept, tested and moved forward.
New debate papers are read automatically each week, checked twice, and placed on the safety case.
The safety-case colours change as evidence arrives.
Stage 3
Prover
One Lean library of the core debate theorems: PSPACE, doubly-efficient debate, cross-examination, stability.
Every theorem's conditions are checked by a machine.
Stage 4
Experimenter
Run the 5 suggested experiments, cheapest first, and design experiments for the other empirical gaps.
Evidence for the empty steps.
Stage 5
Author
A public "state of evidence for debate" review, generated from the atlas and refreshed as it changes.
The atlas's results reach the field.
What to move:14 steps with no evidence, and28 with weak evidence
Other areas
Each area goes through the same pipeline debate went through. What matters most is a published safety case or framework to rank its gaps against, like Buhl et al. for debate.
Pick 30–50 key papers→Quote them line by line→Map their open questions→Attack the gaps→Two blind checks→Pictures and agent access
The most suited to Lean, so it gains most from the 997 formal records already in place.
Across areas
new
Spine: the 30 shared assumption families
Link areas through the assumptions they share, so a result in one shows where it does or does not carry over to another.
Proposal · not built yet
What could come next
A few ideas for what the atlas could become, set against what it already has.
A
A few ideas worth taking
IdeaAtlas todayWhat we would add
Compare definitions firstToday: 59 debate definitions quoted; not yet compared across paperspartlyOne page per concept: each paper's definition side by side, and exactly where they agree or differ.
Let support flow upToday: the proof graph shows what an error breaks downstream; support does not flow up yetpartlyWhen a step is proved or measured, the steps above it in the safety case update, the way errors already flow down.
Organise by shared structureToday: organised by paper and by topicnot yetViews built around games, information channels and constrained policies, showing which assumptions let results connect across areas.
Use proofs as inputsToday: 13 Lean projects checked; not yet mined for reusable piecespartlyMine proofs for reusable lemmas and for the assumptions that actually carry the weight.
Credit ideas, count reuseToday: every record cites its source line; AI-made results don't say whose idea they build onpartlyRecord whose idea a result builds on, with AI-proposed ideas marked provisional, and count how often each result is reused.
partly in placenot yet
B
Three additions, drawn
Three of the ideas, mapped onto the atlas's own data.
1
An understanding card for each key result
Six short fields in the existing inspector. Two exist already, three can be assembled in part, and only the key idea is new writing. Start with the results the safety case leans on.
1Why it mattersthe safety-case steps it supports and its question's rank
2What it says, plainly and preciselysummary plus the exact quote; the Lean statement where one exists
3The key ideanew writing, AI-drafted and labelled as such
4Which assumptions matter, with a counterexamplehypothesis lists on 243 of 248 results; counterexamples from the Lean audits
5What it lets us conclude about an AI systemeach result's setting and limits (241 of 248 results)
6What remains openthe 'what remains' line of each of the 33 questions
2
Stress-test one assumption: what still holds if training falls short?
The safety case assumes training reaches an equilibrium, a point where neither debater can do better by changing strategy. 15 of its steps rest on that, and only 6 results in 4 papers address it. A stress test loosens the assumption one notch at a time and settles each question mark with a proof, a counterexample or an experiment.
New result→Lean check→Blind read-back→Prior-art search→Counts
AI-proposed results stay marked provisional.
As assumedLocal onlyStops early
Training reaches an approximate global equilibriumclaim??
Training converged to a local equilibriumclaim??
Reached local equilibrium is globalclaim??
Training stuck in a local minimumway the argument could fail??
Training finds efficient equilibrium debaters efficientlyclaim??
Exploration hacking is the main failureclaim??
Convergence time prohibitive, e.g. ELK problemsway the argument could fail??
Models are gradient hackingway the argument could fail??
Empirical tests of debate's key assumptionsopen problem??
Error rate does not drift in deploymentclaim??
A's error rate is at most εclaim??
Equilibria approximate big computation Mclaim??
Game equilibria are mostly correctclaim??
A is not exploration hackingclaim??
How serious is exploration hacking?open problem??
assumed today?unknown: the stress test's job
3
Pick the work by what is actually blocking
Before an agent starts, name what would move the question: a definition, a proof, a statement match, system evidence, a measurement or an explanation. Many to-do items already carry a label that fits.
The 9 mixed questions get split first. Counts are items whose current label fits; each still needs a one-by-one check.
Ambiguous definition→Compare the papers' own definitions21 ambiguities found in the papers
Missing implication→Find a proof or a counterexample22 proof gaps, 4 mathematical questions
Unclear paper-to-Lean match→Review the statements and the definitions they use31 flagged differences
Unknown system applicability→Inspect code, configuration and tracesnone labelled yet
Unsupported observable prediction→Name the population, the event and the measurement20 empirical questions
Hard to explain→Write a worked example and test comprehensionnone labelled yet
C
The long road: from map to the place AI-safety research is checked
Each stage adds one thing people can do that they could not do before.
You are here
Now
Map
Debate read, graded and attacked once.
A ranked to-do list for debate
1
Trust
Experts confirm the finds; people review a small core.
Stress-test missions; support flows up the safety case.
New results, not just a map
4
Widen
AI control next, then other areas, joined by shared structures.
Results checked across areas
5
Open
Outside researchers' agents take missions, credited by reuse.
Grows faster than one team can
6
Decide
Live safety cases, a transfer check for real systems, ranked experiments.
Decisions rest on checked evidence
The aim: the place you check before you cite, build on or rely on an AI-safety result.
D
One database, many applications
A reusable master database connecting theory, AI-safety research, formal results, implementations and evidence. Applications grow from that shared foundation instead of each building its own.
Empirical evidence248 debate results graded by their evidence; 152 rest on one setting
Implementationsa toy debate system, one ControlArena case and one open-model oversight study
Formal results997 Lean and Metamath records; 13 Lean projects machine-checked
AI-safety research657 debate records from 42 papers read in full; 96 on 22 other topics
Theory59 definitions and 27 theorems quoted from the debate papers
One shared foundation
live todaycould be builtlayer startedlayer thin
E
Questions people could bring to it
Real questions, answered from the atlas as it stands. Each answer stays one click from its source.
A researcher
“Can I build on Theorem 2 of Anil et al. 2021?”
Not as stated: a Lean audit found it fails for one order of moves. The atlas shows the line, the counterexample and every result that leans on it. It is an AI draft, not yet confirmed by an expert.
The ranked open questions, what blocks each and the records each needs, as files an agent can read. Writing results back is not open to outside agents yet.
A bonus for AI safety itself. The atlas's own pipeline, AI doing the work under checks tested on planted errors with people reviewing a small core, is a working test of scalable oversight. Logging how well it holds up is evidence in its own right.
It counts as useful only if researchers find the right sources faster, catch missing assumptions, avoid invalid transfers, reuse its exports and send corrections. Record counts don't.