Home

Alignment Workspace

How can a powerful AI develop in line with humanity's interests without relying on control — and how can we get mathematical guarantees that it does? Concretely: how can a reasoner improve without treating every correction as one more signal to optimize around, and how can a person use a more capable future process without giving that process the power to decide what counts as a valid correction?

This research program studies those questions together. Learning from reasons is harder than optimizing a fixed objective because the relevant reasons, permissions, challenges, and standards may themselves change. Being corrigible is harder than predicting or obeying a person because a system can preserve the appearance of consultation while removing the person's effective role.

The program has two research lines and one bridge, with a third line, decision theory, beside them in the repository:

• Normativity asks when a reasoner counts as responding appropriately to reasons and improving within a public practice.
• Deference asks when a more capable reasoner can safely trust and preserve a future human-guided process; its consumer is the legitimate-deference stack, and its dynamic-competence layer is Continuation BRIA.
• Legitimacy asks what must remain true of that process so deference does not merely preserve manipulation, self-authorization, or corruption. Its generic theory is canonical: legitimacy is a property of a trajectory within an interaction whose channels of influence are declared, with an internal half — an Integrity evolution of the accounted obligation state, and authorship of its verdicts — and an external half — the trajectory robustly open at every state, and every channel of influence transparent to its declared reference.
• Decision theory specifies what a computable agent combining logical induction with bounded inductive rationality must satisfy (projects/decision-theory/); it has no wiki page of its own. Diachronic Answerability is derived from the record half, normative induction is the quantitative half, and the Normative Inductor is its conditional realization.

The bridge matters because good bookkeeping is not enough. A record may track every debt while the surrounding process prevents a challenge from reaching its target. Conversely, a corrective power may remain causally available while the system gives it no legitimate standing. The work separates these properties before asking how they compose.

Where to start

New to the project: read Why normativity? for what problem this is, then Architecture for the common shape, then follow either Normativity or Deference.

Returning after time away: Legitimacy carries the canonical theory in ten steps and links each component to its page; the legitimacy spine of the normativity claims registry is its statement of record, and the decision ledger records what has been ruled since.

Looking for the mathematics: the Theorem Spine states the program's results at theorem level — hypotheses, conclusions, Lean names, and the strength each one actually has — from the account calculus through Progress, legitimate deference, corrigibility and continuation BRIA.

Looking for current research status: read the status section on the relevant line and then Roadmap. Each technical page ends with immutable links to the underlying evidence.

How to read status

• Established — epistemic class means a claim is registered in the workspace and repeats its exact class: lean-proved, enumeration-verified, witness-checked, contributor-checked, or test-supported.
• Open / unregistered covers both unanswered questions and current research results that have not crossed the workspace's explicit promotion boundary. The page states which is which.
• Aspirational describes a research direction and claims no mathematical backing.

The normativity line's traderization results, the record half of the legitimacy spine, and the deference line's finite results are registered and carry lean-proved; the corrigibility nucleus — corrigibility as faithfulness to an allocation of authority, with the lexical protected-authority theorem as its incentive half and legitimacy entering through the segment gate — is stated in Lean and unregistered. Everything else discussed here is open, a living note, or unregistered research: its round verdicts and evidence strengths are preserved, and the wiki does not upgrade any of it to Established. The legitimacy theory is canonical and its remaining work is realization; the deference line's older target waits on one decision, the succession of item 28 <a class="ref item" href="/items/28/">[item 28, closed]</a>, and its temporal-depth half is supplied by continuation BRIA.

Wiki and lab

This wiki is the human-facing conceptual register. The repository is the lab: proofs, experiments, statements of record, structured state, and verification live there. Evidence links in the wiki use immutable commit pins; the repository's rules and state, not the wiki, instruct contributors and agents. These pages are themselves kept in the repository, under wiki/, and changes to them arrive as pull requests.