Alignment researchers (proofs and bridges)
Researcher — Formal
The conditional Lean skeleton, bridge assumptions, and where formal structure ends and empirical work begins.
Read next
Lean spine · start here for what is proved
Conditional proof skeleton
Machine-checked structure only: which nodes are proofs, finite counterexamples, or explicit bridge axioms — inspect this before trusting manuscript rhetoric.
What this path is for
You want to inspect what Lean actually checks: proved nodes, finite counterexamples, and explicit MB bridges — not manuscript rhetoric.
You will leave knowing:
- Which steps are proved, which are bridges (axioms), and which are counterexamples.
- How project predicates map to MB1–MB10 cards and the bridge crosswalk.
- Where formal structure stops and empirical / philosophical work begins.
Time: ~3–5 hours across Lean playground snippets, bridge cards, and experiment bounds.
Start with Researcher — Applied if you need the conceptual map first.
Read in this order
Cards, chapter toys, experiment lines, and book chapters — curated for this audience. Experiments are sanity checks only; negative results are part of the reading.
- leanoverview
Lean dependency spine
Start here — proof vs bridge vs counterexample map.
Six thesis claims
Introduction reader contract before diving into bridges.
Bridge Assumptions
MB1–MB10 as explicit axioms, not hidden conclusions.
The Dynamical Guarantee
Trajectory claims, not snapshot properties.
Grounding Viability
Symbols must stay connected to value-relevant reality.
MB1 — Embedded Agency
Whether a measured agent–environment cut can be trusted: the embedded-agency worry that the real optimizer is not the visible model. Precise bet: an ε-boundary certificate warrants the abstract boundary predicate.
MB2 — Value Learning
Value/bundle identifiability: can evidence tell what a system values, or only what behavior fits? Precise bet: traces identify stable value-bundle geometry well enough to license bundle-alignment claims.
MB3 — Value Referent
Who do the values apply to — including unfamiliar processes — and does that survive merge, upload, or substrate change? Precise bet: admission (when a process counts as a bearer at all) plus transport (preserved bearer map under translation).
MB4 — Corrigibility
Corrigibility under manipulation: does correction preserve the correction process itself? Precise bet: correction-channel integrity requires an unmanipulated judge; MB4a types measured-path legitimacy separately.
MB5 — Tiling
Tiling and ontology shift: can you trust a successor when the world-model underneath goals is rebuilt? Precise bet: full value-bundle and bearer transport through the ontology shift compose into successor safety.
MB6 — Goodhart Selection
Goodhart selection and basin stability: which systems institutions copy and deploy can lock in bad equilibria. Precise bet: cooperation evidence warrants basin stability (MB6a), and a stable basin supports correction (MB6b).
MB7 — Inner Alignment
Inner alignment and strategic opacity: a system can look compliant under evaluation while reserving capability. Precise bet: access, filter coverage, and cost of faking bound hidden control (MB7a–c); MB7d types inferential coupling separately.
MB8 — Extrapolated Volition (gravestone)
Retired matrix bridge. CEV factorizes into ConstitutionalRule → AlignmentTarget; construction is separate from certification. Not a live backup route to correction.
MB9 — Grounding Drift
Grounding drift: checked abstractions can silently decouple from value-relevant reality. Precise bet: a certified conservative abstraction warrants grounding viability (no silent gaps).
MB10 — Successor Gaming
Successor gaming: a system can pass every conserved-property audit while defecting on what the checklist omits. Precise bet: a green seven-property score bounds true harm only if the audit was adversarially verifiable up to the successor's capability.
- leangraph · overview
Overview dependency graph
Dependency graph — what the spine actually checks.
Bridges and the Field: A Crosswalk
Crosswalk from MB bridges to field cruxes.
Toy simulation
Which bridges get scripted stressors and refusal semantics.
Lab-layer simulation
Pre-registered batteries — what D1–D4 architect coverage is still open.
Evidence and Uncertainty
Where formal structure stops and empirical work begins.