The Discovery Loop

How the AI-driven harness self-drives, where it fails, and what the methodology generalises to

BEDC is run by one human and a Codex agent loop. 1837 theorems in 72 hours. Here is the engineering — including the failures that taught us how to build it.
Author

The Omega Institute

Published

May 2, 2026

中文

A theorem that should not enter the codebase

theorem abgroup_mul_middle_four
    {mul : BHist -> BHist -> BHist}
    (assocC : forall x y z, hsame (mul (mul x y) z) (mul x (mul y z)))
    (commC  : forall x y, hsame (mul x y) (mul y x))
    ...
    forall a b c d, hsame (mul (mul a b) (mul c d)) (mul (mul a c) (mul b d)) := by
  ...

This kind of theorem has four problems:

  1. The name suffix _four is forbidden by NAMING.md §3 — mechanical-arity expansions like _two/_three/_four/_five/_six are explicitly banned.
  2. The hypotheses (assocC : forall x y z, hsame ...) and (commC : forall x y, hsame ...) are pure parameter-echo: the theorem assumes its own conclusion’s structure as input.
  3. The proof body composes those parametric hypotheses with no reference to a concrete BHist constructor.
  4. The prompt-level lint — explicit grep -E '_four\b' — should catch this and abort the commit.

Soft prompt instructions are not reliable; codex can skip them. The slop can enter the codebase.

This is not an isolated failure. It is the kind of failure that taught us how the harness actually has to be built.

The basic loop

The project runs two parallel pipelines:

Pipeline Script What it does
R rounds (Lean) lean4/scripts/codex_formalize.py Picks formalisation targets, writes Lean proofs, registers paper markers, commits
P rounds (Paper) papers/bedc/scripts/codex_revise.py Audits paper drafts, proposes theory extensions, edits LaTeX, commits

Both pipelines run via the Codex CLI on isolated git worktrees in parallel. A single human (the project author) supervises by reading commit batches, running audits, and tightening constraints when slop patterns emerge.

The throughput at peak: ~500 commits per day, split roughly evenly between the two pipelines. Most commits add 10-50 lines of Lean or LaTeX. The pipelines do not generate completion claims, summaries, or status reports — only tightly-scoped commits that pass a fixed set of audits.

The audit gates

Five mechanical audits run per commit, all from tools/check-axioms.py and lean4/scripts/bedc_ci.py:

cd lean4 && lake build                               # 0 error
python3 tools/check-axioms.py                        # 0 axiom keyword
grep -r "sorry" lean4/BEDC --include="*.lean"        # 0 sorry
python3 lean4/scripts/bedc_ci.py audit               # paper ↔ Lean drift = 0
python3 lean4/scripts/bedc_ci.py axiom-purity        # transitive purity (1837/1837 pure)

The axiom-purity check is the strictest: it runs #print axioms on every BEDC theorem and refuses dependencies on Classical.choice, Quot.sound, or propext. Currently 1837/1837 theorems pass. This is a stronger constraint than mathlib4 or any standard Lean project.

Failure Modes And Control Surfaces

The harness does not stand on one prompt. It needs layered control surfaces, each blocking a different path of least resistance.

Soft preferences: try-close, cross-domain abstraction, single-concept commits

Coverage-sweeping commits touch multiple unrelated domains, each adding a parameter-echo theorem. The taste audit identifies three preferences to push back:

  1. Try-close before adding — verify the candidate isn’t already provable by simp / induction on existing primitives. One-step-from-existing “theorems” belong inline.
  2. Cross-domain abstraction priority — when \(\ge 3\) horizons already prove the same shape, the next target is hoisting the shape into a typeclass, not adding a fourth concrete instance.
  3. Single-concept rounds — prefer 3 targets that develop one concept on three objects, rather than coverage sweeps spanning unrelated concepts.

These are prompt-level soft preferences. They move the needle slightly but do not stop the slop.

Derived shape saturation as hard gate

The taste audit also tracks shapes saturated across Derived horizons: _ClassifierSpec_trans, _HistoryClassifier_trans, _HistoryClassifier_hsame_transport, and similar proof patterns can repeat across horizons. Each new horizon can produce yet another copy of the same proof pattern.

bedc_ci.py audit --shape-saturation groups every Derived theorem name by its domain-prefix-stripped suffix and flags shapes reproduced across \(\ge 3\) horizons. When a candidate target hits a saturated shape, the automation must either hoist the shape into a typeclass or pick a different target.

Hard rule, not preference.

Critical-path discovery

Automation tends to attack the same easy horizons and never open new fronts. Horizons with few theorems and many downstream dependents can receive no traffic unless the scheduler forces attention.

lean4/scripts/critical_path.py scans every horizon chapter, extracts the dependency graph from \<X>Up references, computes transitive downstream count, and ranks transitive_downstream / (1 + thms) after excluding nodes that are saturated or whose deps are not yet ready.

Formalisation target selection must call it and choose at least one target from the top nodes.

$ python3 lean4/scripts/critical_path.py
{
  "top": [
    {"name": "abgroup",  "thms": 2, "downstream": 4, "score": 1.33},
    {"name": "monoid",   "thms": 5, "downstream": 4, "score": 0.67},
    {"name": "real",     "thms": 0, "downstream": 3, "score": 3.00},
    ...
  ]
}

This shifts commit subjects from “another easy horizon closure” toward horizons with larger downstream impact. The harness starts opening new fronts on its own.

Tighten the fallback

A soft “if technically blocked, use fallback targets” escape lets codex rationalise every deviation as blocked.

The blocker definition must be mechanised. A top node counts as blocked only when ALL THREE of:

  1. The paper chapter has < 3 \begin{definition} blocks, AND
  2. Implementation needs a Lean inductive or import that does not yet exist, AND
  3. critical_path.py reports deps_ready = false.

If the top nodes all claim blocked under that conjunction, codex must emit {"targets": []} and skip the commit. Empty commits are preferred over silent fallback.

This turns “I was blocked” from a story into a checkable condition.

Phase D mechanical lint (and the dilemma it raised)

Even with critical-path scheduling and blocker definitions, abgroup_mul_middle_four-style slop and parameter-echo schemas can still enter the codebase. Prompt-level instructions to grep are unenforceable: codex can simply not run the grep.

We added lean4/scripts/phase_d_lint.py (split from a previous in-pipeline lint). It runs three checks on every commit’s added Lean blocks:

  1. Mechanical-arity suffix: any new theorem _foo_(two|three|four|five|six) is rejected.
  2. Parameter-echo binding: any new theorem with a hypothesis (name : forall ... hsame ...) is rejected — the theorem is taking its own conclusion’s structure as input.
  3. BHist anchor: any new BEDC.Derived.* theorem whose statement does not mention BHist, BMark, hsame, Cont, ProbeBundle, etc. is rejected — it is not actually about kernel objects.

The dilemma: this is a mechanical override of the prompt path. The author’s preference is “fix the prompt, don’t bolt on a guard”. Phase D lint is a guard.

The compromise we landed on: keep Phase D, but as a floor, not a primary mechanism. The primary mechanism is still prompt: critical-path priority, saturation gate, anti-hollow. Phase D catches the cases where codex decides to ignore the prompt. This is the “trust but verify” architecture.

Schema-only horizons exclusion

The deepest insight came from auditing the parameter-echo failures. The pattern was: every abgroup / monoid / ring / field round produced parameter echo. Why?

Because the paper schema of those chapters writes laws as \(mul : BHist \to BHist \to BHist\) left abstract. There is no concrete carrier. Codex was correctly trying to formalise what the paper said, and parameter echo was the only shape that could compile against that schema.

The fix is not a tighter lint. The fix is to recognise the paper schema as the upstream cause and exclude these chapters from the critical-path top until the paper itself adds concrete carrier definitions.

# critical_path.py
SCHEMA_ONLY_HORIZONS: set[str] = {
    "abgroup", "group", "monoid",
    "ring", "commring", "field",
    "module", "vecspace", "linearmap", "matrix",
    "polynomial", "fps",
    "lattice", "totalorder", "preorder", "poset",
}

This is the architectural lesson of the project so far: when the formalisation pipeline produces consistent slop, the cause is often upstream in the spec, not in the prompt or the agent.

What the loop actually does

After all the upgrades, the day-2 loop looks like this:

Phase B
codex runs critical_path.py, gets top-3 horizons, picks ≥1 target there. Saturation audit runs against candidate names. Anti-hollow rules filter out parameter-echo candidates.
Phase C
codex writes Lean proofs. lake build must pass. Paper marker gets registered. Single combined commit.
Phase D
Mechanical lints (arity, parameter-echo, BHist-anchor) run as a final filter. bedc_ci.py audit + axiom-purity verify alignment. Round merges to base.
Human (occasional)
Reviews ~10 commits per session, names patterns codex didn't notice (Hom = Cont, S¹ as equation-as-BHist, etc), writes them up as bridge theorems or reflective sections.
Discovery
Bridge theorems sit in papers/bedc/parts/visions/ — a directory whose existence is the only structural commitment to "cross-chapter unifications get a home".
🧑 Human 🤖 AI 💡 Discovery

The human’s contribution per session is ~30 minutes of review + ~5 lines of prompt edit. The AI’s contribution per session is ~50 commits.

Capstone bridges — turning observations into theorems

The most recent harness upgrade addresses a question the discovery pattern keeps raising: when the AI does produce a cross-chapter unification observation (like Hom = Cont), what should happen to it?

Earlier proposals: write it up as paper prose in a meta-commentary chapter. Rejected. That is annotation alongside the theory, not theory itself.

Current mechanism: when a theory_extension candidate has cross_chapter_unification = 2 (cites \(\ge 3\) leanchecked names from \(\ge 3\) chapters AND the conclusion is an equivalence/iff/bridge), it gets absolute priority over ordinary candidates. Its paper_files[0] lands in papers/bedc/parts/visions/. The bridge theorem is itself a Lean theorem, not a prose paragraph.

\section{Continuation as Category Morphism}
\begin{theorem}[Hom carrier as restricted continuation]
\label{thm:capstone-hom-cont}
For all histories $a, b, f$,
$$
  \mathsf{CategoryHomCarrier}(a, b, f)
  \iff
  \mathsf{UnaryHistory}(a) \land \mathsf{UnaryHistory}(b)
  \land \mathsf{UnaryHistory}(f) \land \mathsf{Cont}(a, f, b).
$$
\end{theorem}
\leanchecked{BEDC.Derived.CategoryUp.CategoryHomCarrier\_iff\_unary\_cont}

Reflection becomes formalisation. AI synthesis becomes Lean theorem. The bridge is verifiable, not just narratively claimed.

What the methodology generalises to

The pattern that extracted from BEDC is not BEDC-specific. We think it applies to any project where:

  • A human defines a kernel with strong invariants (no axioms, mathlib-free, axiom-purity, etc).
  • An AI agent is asked to do bulk formalisation against that kernel.
  • The kernel’s invariants are mechanical (#print axioms, lake build, etc).
  • A small human review loop catches the cases where the agent’s output is technically valid but architecturally noisy (parameter echo, saturated shapes, etc).

The recipe:

  1. Mechanical floor: kernel + audits + Phase D lints. Without these, the AI can produce arbitrary slop and you cannot detect it.
  2. Critical-path scheduling: do not let the AI choose what to work on by local greed. Force selection through a global function (downstream impact / scarcity / deps-readiness). The AI is good at execution; bad at strategic prioritisation.
  3. Schema-only diagnosis: when the AI keeps failing in one area, the cause is often upstream in the spec, not downstream in the agent.
  4. Capstones, not annotations: when the AI produces synthesis observations, formalise them as theorems, not prose. Otherwise they decay into commentary.
  5. Human as architect, not reviewer: the human’s job is to set invariants, name unifications, and tighten the harness. Not to peer-review proofs (the audits do that).

What this is not

This is not a claim that AI will replace mathematicians. The architectural decisions in BEDC — inductive BHist | Empty | e0 | e1, the axiom-purity invariant, the schema-only diagnosis, the recognition of Hom = Cont as a unification — were all made by a human. The AI does the bulk of the formalisation work, but the direction is human.

This is also not a claim that the harness is finished. We expect another five iterations of upgrades before it stabilises. Each upgrade so far has been driven by a specific failure mode, and there are failure modes we have not yet hit (e.g. capstone-bridge slop is still untested in volume).

This is a claim that, with a 250-line Python harness and ~1500 lines of prompt, one human can supervise an AI agent producing 1837 mechanically verified theorems across 38 chapters of foundational mathematics in 72 hours. That number is real. The bottleneck is not AI capability; it is the human’s ability to architect invariants and name unifications.

← Back to the main story
What BEDC is, what happened in 72 hours, and the five surprises that came out of the AI-driven formalisation. Default Failure Modes →
The cognitive shape underneath the failures the harness was built to absorb — what AI agents produce when nothing pushes back. Distinction as Foundation →
The philosophical position: why we think e0/e1 is more primitive than sets, types, or categories.

— The Omega Institute