Research Agenda: Building an Agent System for Birational Geometry

Figure

Figure. Design sketch, not an as-built system. The upper band is the mathematical control state: a coupled theorem package is advanced by creating the right lower-dimensional object, checking its hypotheses, and admitting only verified updates. The lower band maps the agent-design patterns to the research workflow. Solid navy arrows show control, dashed teal arrows show evidence or repair feedback, and red arrows show a correctness or admission gate.

Status of this page. This is a domain-specific research architecture and a long-term implementation target. It is not a claim that Danus, Rethlas, or any current system already implements the complete birational-geometry workflow shown here.

The objective is not only to build an assistant that explains known mathematics, but to build a system that can eventually solve selected real birational-geometry problems. A successful solution must include a precise statement, a dependency-complete argument, checked hypotheses, and enough provenance for a mathematician to inspect and challenge it.

The central architectural idea is that birational geometry should not be represented as a single linear “question → proof” pipeline. A research episode often changes representation: a pair may be replaced by a log-smooth model, a divisor may be restricted by adjunction, or a fibration may expose a lower-dimensional base. The agent must preserve those changes as explicit, typed obligations rather than hiding them inside a long conversation.

1. Spiraling induction as the mathematical control policy

Here “spiraling induction” refers to the BCHM-style proof organization recorded in the birational-geometry notes: several statements are proved together in dimension $n$, while some steps manufacture an object in dimension $n-1$, apply the lower-dimensional package, and use the result to advance the current package. It is a mathematical proof architecture, not a standard AI design pattern name.

For the BCHM package, the useful abstract dependency shape is:

The important engineering consequence is not to encode these symbols as labels only. Each edge needs an obligation record containing:

• the statement being attempted and its dimension;
• the object that has to be constructed before induction applies;
• the hypotheses that must be rechecked on that object;
• the evidence and proof artifact supporting the implication; and
• the next obligations unlocked by an accepted result.

The system therefore spirals in two senses: it revisits a coupled theorem package, and it moves between dimensions or derived objects while preserving a machine-readable ledger of what has actually been established.

2. Geometric engines of the spiral

The main tools are geometric transformations, not generic Agent tools. They manufacture a new object on which an inductive theorem may be applied, then transfer the conclusion back to the original problem. The system should treat each transformation as a typed GeometricReduction record containing the source pair, the map or center, the target dimension, the transformed pair, the relation between adjoint data, the hypotheses checked, and the unresolved conditions.

Adjunction and subadjunction

Adjunction restricts an adjoint expression to a divisor or a suitable stratum, producing a lower-dimensional pair. Subadjunction is the higher-codimension version used around a minimal log-canonical or non-klt center; under the relevant hypotheses it produces a generalized pair on the center. See the adjunction discussion in the Hacon–McKernan–Xu notes, §3.2. In both cases the agent must record the center, normalization, induced boundary or nef part, and the singularity statement that makes the next induction step legal.

Canonical bundle formula

For a suitable fibration $f\colon X\to Z$, the canonical bundle formula transfers adjoint data to the base in the form \(K_X+B+M_X \sim_{\mathbb{R}} f^*(K_Z+B_Z+M_Z).\) The discriminant part $B_Z$ records singularities of the fibers, while the moduli part $M_Z$ records the remaining variation, as formalized for lc-trivial fibrations in Ambro’s work. This is not merely a change of notation: the base pair and the positivity of its moduli part must be constructed and checked before a lower-dimensional theorem can be invoked. The Hacon–Xie proof gives a recent Kähler example in which the canonical bundle formula is an explicit ingredient of the inductive argument.

MRC and Iitaka fibrations

The MRC fibration is the natural branch when non-pseudo-effectivity of the canonical class leads to uniruledness: its general fibers are rationally connected and its base has smaller dimension. The agent should route the resulting base problem separately from the fiber problem, rather than flattening the fibration into one prompt.

The Iitaka fibration is the corresponding positive-Kodaira-dimension mechanism when the relevant linear series or semi-ampleness is available. Its base records the Kodaira dimension and its general fiber has Kodaira dimension zero. It must not be invoked before the system has established the positivity, abundance, or finite-generation assumptions needed to define the fibration; see the standard treatment in Lazarsfeld’s Positivity in Algebraic Geometry I.

MMP and scaling as the bridge

Adjunction, subadjunction, and fibrations often require a suitable model first. An MMP with scaling, a dlt or log-smooth modification, and the negativity lemma are therefore bridge mechanisms: they change the model while preserving the precise numerical or birational relation needed by the target theorem. A research agent must distinguish a model change from a proof of the target statement.

The spiral can consequently be read as:

target obligation → choose geometric engine → construct transformed pair or base → verify hypotheses → invoke lower-dimensional result → transfer and record the update.

3. The pattern is broader than BCHM

The theorem graph is not universal: BAB and the Kähler results of Hacon–Xie do not use the same labels or the same technical objects. What recurs is the architecture of the proof: a family of coupled claims, a representation change that makes an induction hypothesis applicable, a hypothesis audit, and an output that feeds a later claim.

The Hacon–Xie case is particularly close to the proposed control model. Their proof separates the big and non-big cases, uses adjunction or an MRC/Mori-fibre space base to reach a lower-dimensional problem, and then returns the result to the original space. The agent should therefore store the construction of the induction object as a first-class artifact, rather than treating “apply induction” as a black-box action.

4. Proposed architecture

Read the upper band of the figure first. The supervisor does not ask a worker to “prove the theorem” in one shot. It selects one frontier obligation, asks what object would make the next theorem applicable, and routes the obligation to the appropriate specialists. The verifier then checks both the proposed mathematical artifact and the conditions for using it.

The lower band is a composition of the patterns developed in this course:

1. Plan-and-execute decomposes a target into a bounded sequence of obligations rather than free-form subgoals.
2. Routing chooses between literature recovery, example construction, proof synthesis, formalization, counterexample search, and human review.
3. Parallelization runs independent searches only when their outputs can be normalized and compared.
4. Structured output makes every worker return an obligation, evidence packet, derivation, counterexample, or verification report with a fixed schema.
5. Knowledge retrieval and provenance preserve theorem statements, hypotheses, page or section information, and the exact source of a claim.
6. Reasoning and representation change treats adjunction, fibrations, restrictions, models, and numerical conditions as explicit transformations.
7. Reflection and recovery turn a failed hypothesis check into a repair task, not an unsupported revision of the conclusion.
8. Memory management stores accepted artifacts and dependency edges, not merely the raw transcript of the agent.
9. Human-in-the-loop and guardrails reserve mathematical interpretation, research significance, and final admission for an explicit checkpoint.

5. Typed research artifacts

The architecture becomes auditable only when its intermediate objects are stable. A minimal artifact vocabulary is:

An artifact should carry a status such as proposed, needs-hypothesis-check, rejected, verified, or human-accepted. Only the last two states may unlock the next stage, and a verified result should still record which verifier and which assumptions produced that status.

6. One spiral episode

For one frontier obligation, the control loop is:

1. Select the frontier. The supervisor chooses the highest-value unresolved obligation under a dimension, dependency, and resource budget.
2. Compile the obligation. The planner writes the target statement, dependencies, and the object that must be manufactured before the induction hypothesis can be invoked.
3. Route and explore. Specialists search the literature, inspect examples, test boundary cases, and propose a proof or reduction in parallel where independence is genuine.
4. Normalize. The system converts the results into typed evidence packets and derivations with explicit hypotheses and provenance.
5. Check the representation change. A dedicated verifier checks that adjunction, restriction, fibration, birational modification, or dimension drop has been stated correctly and that the new object satisfies the needed assumptions.
6. Verify and repair. Logical, symbolic, formal, and citation checks either produce a repairable failure or a candidate admission report. A human may inspect the interpretation when the mathematical stakes require it.
7. Commit the update. The ledger receives the result only through an admission gate. The update unlocks the next obligation and starts the next turn of the spiral.

This gives the system a meaningful stopping rule: stop when the target package has a verified dependency path, or stop with a precise unresolved obligation when the evidence or hypotheses are insufficient. “The model produced a plausible proof” is not a termination condition.

7. Domain-specific pattern map

The interfaces are deliberately mathematical rather than framework-specific. An implementation could change its language model, retrieval backend, or formal checker without changing the contract of an obligation or verification report.

8. Reliability boundaries

The proposed system may search, compare, formalize, test, and suggest. It must not silently:

• apply an induction hypothesis before recording the dimension drop;
• replace a pair without rechecking singularities, positivity, or coefficient conditions;
• confuse numerical equivalence, linear equivalence, and actual equality;
• treat a citation as evidence that its hypotheses apply to the current pair;
• promote a fluent proof sketch into the induction ledger; or
• treat an unresolved counterexample search as evidence of truth.

These boundaries are the domain equivalent of the correctness gate seen in the Danus and Rethlas code case study: generation and verification are separate responsibilities, and admission is an explicit state transition.

9. A realistic first implementation

The safest first vertical slice is deliberately narrow:

1. define the ResearchBrief, Obligation, EvidencePacket, and VerificationReport schemas;
2. implement a supervisor that advances one small theorem package at a time;
3. add retrieval with source locators and hypothesis extraction;
4. add example and counterexample workers before adding many autonomous proof writers;
5. require a human review for every ledger update during evaluation; and
6. measure hypothesis accuracy, provenance completeness, repair usefulness, and false-admission rate on a fixed collection of known arguments.

Only after this slice is reliable should the system add broader exploration, more agents, or expensive formal verification. The architectural objective is not maximal autonomy. It is a trustworthy research instrument whose next step, evidence, and reason for stopping can all be inspected.

10. What “solve a real problem” should mean

For this research programme, “solve” should be an operational claim rather than a marketing label. A candidate solution should produce:

• a precise theorem or counterexample statement;
• a complete dependency graph of the lemmas and external results used;
• an explicit record of every representation change, dimension drop, and hypothesis check;
• a reproducible verification report, including failed approaches; and
• a human-readable mathematical argument that survives expert review.

The validation ladder should therefore move from controlled to genuinely open work:

1. Proof replay: reconstruct known arguments and recover their dependency structure from source material.
2. Bounded problem sets: solve examples, special cases, and counterexample searches with known answers.
3. Research-grade reconstruction: complete missing steps in published or partially formalized arguments under human supervision.
4. New mathematics: attempt unresolved problems, while reporting clearly which parts are verified, conjectural, or still open.

The final stage is the scientific goal, but the earlier stages are necessary to measure false admissions, missing hypotheses, unsupported citations, and the system’s ability to recover from a wrong branch of the spiral.

References

1. C. Birkar, P. Cascini, C. D. Hacon, and J. McKernan, “Existence of minimal models for varieties of log general type,” Journal of the American Mathematical Society 23 (2010), 405–468. AMS article and arXiv version.
2. C. Birkar, “Singularities of linear systems and boundedness of Fano varieties,” Annals of Mathematics 193 (2021), 347–405. Journal article.
3. C. Hacon and L. Xie, “On the Kähler MMP and the transcendental base-point-free theorem,” arXiv:2607.24986 (2026), especially Sections 1.1–1.2. Paper and HTML version.
4. J. Liu et al., “Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory,” arXiv:2607.06447 (2026). Paper and source repository.
5. H. Ju et al., “Automated Conjecture Resolution with Formal Verification,” arXiv:2604.03789 (2026). Paper and source repository.
6. A. Gullí, Agentic Design Patterns: A Hands-On Guide to Building Intelligent Systems, Springer, 2025. Publisher record.
7. V. Dibia, Designing Multi-Agent Systems: Principles, Patterns and Implementation for AI Agents. Author’s book site.
8. F. Ambro, “The moduli b-divisor of an lc-trivial fibration,” arXiv:math/0308143. Paper.
9. R. Lazarsfeld, Positivity in Algebraic Geometry I: Classical Setting: Line Bundles and Linear Series, Springer, 2004. Publisher record.
10. C. D. Hacon, J. McKernan, and C. Xu, Boundedness of varieties of log general type, expository notes, Section 3.2 on adjunction. Notes.