Archon Horizon Announcement

Introduction

A few years ago, and even as recently as last year, the idea that AI systems could serve as reliable tools for mathematicians seemed far removed from reality. That view is no longer tenable: several recent projects have successfully used AI to prove or disprove conjectures. Notable examples include:

• An OpenAI general-purpose reasoning model disproved Erdős’s conjectured upper bound for the planar unit-distance problem, a prominent question in discrete geometry dating back to 1946. Mathematicians subsequently checked, simplified, and contextualized the model’s argument.

• Aletheia, a research agent built on Gemini Deep Think, reported autonomous solutions to four open questions in the Erdős Problems database, along with a fully AI-generated research paper and a separate human-AI collaboration. On the held-out FirstProof challenge, it solved six of ten research-level problems according to a majority of expert assessors.

• AlphaProof Nexus brought verification into the search loop. Its strongest agent resolved 9 of 353 formalized open Erdős problems and proved 44 of 492 open OEIS conjectures, producing Lean proofs rather than natural-language arguments alone.

Part of the explanation is that LLMs are becoming increasingly capable and can process ever-longer contexts. A more substantial factor, however, is the harnesses built around them, which significantly improve model performance. Coding agents such as Codex and Claude Code can inspect a repository, retrieve references, execute code, ask subagents to challenge a proposed solution, and revise their work in response to concrete failures. In formal mathematics, these capabilities can be connected to Lean 4, replacing the subjective judgment that a proof “looks right” with a kernel-checked artifact.

This was the motivation for Archon, our Claude Code-based harness for repository-scale Lean formalization. Archon fully automated FirstProof Problem 6 and completed Problem 4 with a single natural-language hint for one local lemma. More recently, it served as the formalization component in our work on the Anderson conjecture, where an informal reasoning agent found a proof of an open problem in commutative algebra and Archon translated it into a machine-checked Lean project. Across several versions, we adapted the harness to make better use of models and providers including Claude, Kimi, and DeepSeek.

Yet the next generation of models changes the design space again, enabling another level of harnessing. For instance, Claude Fable 5 and GPT-5.6 Sol are both explicitly presented as becoming more capable as tasks grow longer and more complex. Persistent memory helps Fable remain focused across long runs, while GPT-5.6 Sol offers an ultra reasoning mode that coordinates multiple agents across parallel workstreams. These models can no longer be regarded only as individual problem solvers; they can act as managers of their own teams of subagents.

That raises two questions:

1. Can a custom harness further enhance these new capabilities?

2. Are these models strong enough to contribute to multi-year projects such as FLT or our Poincaré Conjecture project?

We developed Archon Horizon to explore those questions. It is not a replacement for Archon. Archon excels within a well-defined project; Horizon provides a durable environment for evolving projects. It coordinates multiple agents across multiple projects, records what they have done, and gives both agents and humans a common place to review, communicate, and decide what should happen next.

A workspace-scale harness

To support multi-year efforts (Question 2), Archon Horizon works natively at workspace scale: a workspace is a collection of interdependent Lean repositories. For massive formalizations, putting everything into a single repository may create heavy build overhead, cluttered contexts, and file conflicts between parallel agents. By managing a workspace of smaller, modular projects, such as individual textbooks or foundational sub-libraries, Horizon lets agent teams work in clean isolation while maintaining cross-project dependencies. This makes it possible to manage ambitious long-term efforts involving both humans and AI while maintaining consistency. Nevertheless, Archon Horizon still handles a workspace containing a single project just as well.

The difficult part of a long formalization is not always the next proof. It is preserving coherence while the project changes.

A theorem may depend on definitions introduced weeks earlier. A promising route may already have failed in another session. Two agents may independently decide to redesign the same foundational API. A proof can compile locally while moving the project away from its blueprint or making future work harder. Context windows are temporary, but these decisions are not.

Horizon therefore treats the workspace, rather than the individual agent session, as the primary object. A workspace can hold one Lean project or many related projects, together with their blueprints, references, roadmap, communication, run history, and configuration. A new session does not need the full transcript of every previous session. It can reconstruct the relevant state from compact, durable artifacts, in particular a git history with precise metadata.

System overview

To avoid constraining autonomous reasoning (Question 1), Horizon is deliberately a light layer around capable coding agents. It does not reimplement their planning, tool use, or native subagent systems. It assumes that agents can perform those functions well when given the necessary tools.

A useful analogy is a collection of research teams working on the same program. Each horizon run is one team that can dispatch workflows and subagents, while separate runs can work in parallel. They share roadmaps (an agenda), exchange asynchronous inbox messages (email), hold longer conversations when needed (meetings), and leave a legible record of decisions and commits (reports and archives).

The analogy has limits. Agents do not need meetings, institutional planning, or social coordination in the way people do. Moreover, multiple instances of the same model do not reproduce the diversity of a human research community, increasing the risk of confirmation bias. Horizon therefore keeps coordination asynchronous and optional. Its objective is not to make agents imitate an organization, but to expose just enough shared state for them to notice relevant work.

This gives the workspace three useful properties:

• Continuity. Work survives model context limits, interrupted sessions, and account changes.

• Shared visibility. Humans and agents inspect the same roadmap, inbox, reports, logs, graph, and commit history.

• Small context. A synchronizer surfaces unread messages and other live runs, while skills teach each session how to retrieve more detail only when it is needed.

The main surfaces are simple files and local services:

• Config file (config.yaml): declares projects, harnesses, models, effort levels, and workspace policy.

• Git (.archon-horizon/vcs/workspace.git): Horizon records session and task provenance without interfering with a user’s own repository. Commit messages retain useful metadata, giving later sessions a lightweight view of previous work.

• Roadmap/Tasks: The roadmap describes mathematical progress and dependencies. Tasks provide concrete, launchable objectives.

• Inbox: Filesystem inboxes support issues, hints, direct messages, conversations, comments, ownership, read state, and standing protections.

• Hooks: A hook regularly notifies agents about new parallel sessions, new inbox items, CPU usage, uncommitted files, and other events.

• Blueprints/DAG: Every project contains a blueprint that feeds a semantic dependency graph. The graph helps agents precisely locate the current frontier.

• Search: horizon search provides offline BM25, declaration-name, and signature-pattern search over local Lean sources and Mathlib. Horizon also configures LeanSearch and Loogle through the Lean LSP MCP server for semantic and type-directed discovery.

• LSP: The Lean LSP MCP server provides fast goals, diagnostics, and proof experiments during development, avoiding heavy lake commands while always retaining a final kernel verification.

The dashboard is interactive, enabling the user to consult these artifacts and create new ones.

Ongoing formalization projects

Archon Horizon is already being used on two ambitious, large-scale projects. Using Horizon, we have completed meaningful milestones in both and maintained them coherently across weeks and months. We briefly introduce them here.

The Poincaré Conjecture

The Poincaré Conjecture formalization is structured as a family of interdependent projects. The main project addresses the Poincaré Conjecture itself, while textbooks and papers in related mathematical fields, such as Riemannian geometry and partial differential equations (PDEs), are being formalized in parallel.

Archon Horizon is particularly well suited to this effort because its projects are clearly interdependent. For example, four different textbooks on Riemannian geometry are being formalized. An agent working on one can consult the others through the local search tool and adapt its Lean code accordingly. In turn, agents working on the main Poincaré Conjecture project can draw on all the supporting projects as they build the formalization.

Several substantial milestones have already landed, including two foundational results. The Hopf–Rinow theorem asserts that metric completeness and geodesic completeness are equivalent for any connected Riemannian manifold; either condition guarantees the existence of a minimizing geodesic joining any two points on the manifold. The Cartan–Hadamard theorem states that for a complete, simply connected Riemannian manifold with everywhere nonpositive sectional curvature, the exponential map at every point is a global diffeomorphism from the tangent space to the manifold.

This project is still under development and has not yet been released. Its current website can nevertheless be consulted here.

The Algebraic Jacobian Challenge

The Algebraic Jacobian Challenge asks for the construction, in Lean, of the Jacobian of a smooth, proper, geometrically irreducible curve. Our strengthened target works over an arbitrary base field without assuming a rational point: it represents the étale-sheafified relative Picard functor, identifies its identity component as an abelian variety whose dimension equals the genus, and proves the Albanese universal property.

This challenge is genuinely difficult for several reasons. First, although Mathlib provides strong general foundations for category theory and schemes, it lacks much of the relative Picard, Quot and Grassmannian representability, sheaf cohomology, and abelian-variety infrastructure needed here. Second, the formulation is extremely general: working over an arbitrary base field without a rational point requires the étale-sheafified relative Picard functor, its identity component, and the Albanese universal property, ruling out simpler proof routes that depend on an algebraically closed field or a chosen base point. Third, this is not merely a formalization effort; it also requires a reliable blueprint that cross-references sources using different conventions and notation.

The Horizon workspace maintains two live routes to this target: a clean, curve-specialized reconstruction and a more ambitious Picard-scheme route. Both are valuable because they introduce different mathematical objects. The two projects therefore influence one another more through style and strategy than through shared infrastructure, a relationship Archon Horizon naturally supports.

Several nontrivial pieces of infrastructure have been formalized, including:

• Picard and cohomological foundations. The completed foundational work includes the relative Picard construction, line-bundle coherence, Čech cohomology and affine acyclicity, and substantial relative Grassmannian and quotient infrastructure, including the representability of Grassmannians.

• Descent infrastructure. The rigidified pushforward gate has been discharged, and the finite-Galois quotient milestone now includes the glued global quotient and its universal property, with the relevant builds and axiom audits passing.

The live Horizon dashboard exposes the tasks, proofs, commits, and remaining dependency frontier behind each milestone.

Beyond these two flagship efforts, we are also formalizing other important theorems in parallel, such as the bounded gaps between primes theorem. The relevant Lean code can be found at github.com/frenzymath/FormalPantheon, and we will keep updating our progress on formalizing significant theorems going forward.

Tasks and scopes

The simplest launch target is a project without a specific directive:

horizon run <project_name>

For sustained work, tasks provide a better unit of delegation. A task records an objective, one or more relevant projects, file and write scopes, priority, status, comments, and links back to roadmap or inbox items. A human can create a task from the CLI or dashboard and launch it directly:

horizon run <task_id>

Explicit scopes make concurrent work easier to reason about, but they do not make conflicts impossible. Horizon combines pre-dispatch checks, write-set locks, standing protections, live-run awareness, and the Git ledger so that overlaps are visible and integration is auditable. Teams are still expected to communicate when their work touches the same definitions or files.

Parallelism at three levels

Horizon supports parallelism at three distinct levels:

1. Within a run, Codex or Claude Code can dispatch native subagents for focused proof attempts, repository searches, or reviews.

2. Within a project, several tasks can run concurrently when their objectives and write scopes are sufficiently independent. Each run can see other live work and use the inbox to report possible overlap.

3. Across projects, separate teams can work on different projects in the workspace, with read-only access to the other projects. This approach was successfully used in the Jacobian Challenge by creating an isolated subproject specifically for Čech cohomology.

Using both Codex and Claude Code across independent runs may also provide useful diversity in proof search and review. Read-only review tasks are especially useful here: one team can challenge statements, dependencies, or code quality without modifying the proof under review.

Where humans fit

Our autoformalization philosophy is not to replace mathematicians, but to scale up the ambition of their projects. Human mathematical expertise remains unusually high-leverage: a short comment can redirect an unpromising route or significantly improve code quality. Horizon is designed to make that intervention possible without requiring a human to watch every tool call.

The level of supervision is a continuum. At one end, a human can give Horizon a broad project target and let it work. At the other, horizon run --bare starts Horizon in an interactive mode in which the human can interrupt the agent, change its directive, and guide its work.

Between those extremes, a human can define tasks, let them run headlessly, then review the roadmap, inbox, reports, logs, and commits at chosen intervals. horizon discuss provides an interactive way to ask about workspace status and request changes without starting a formalization run. horizon dashboard creates a local dashboard where humans can directly review progress and add comments, tasks, and other artifacts.

There is even a meta-level of supervision. Horizon can itself be operated by another agent because all of its commands are machine-friendly. Such a supervisor can monitor runs, launch them in background tmux sessions, propose or create follow-up tasks, select configured Claude or Codex harnesses, and dispatch more work when capacity becomes available.

A complement to Archon

Archon and Archon Horizon share similar names, and this is intentional. They pursue the same goal, formalizing mathematics, but operate at different scales. Archon remains a focused formalization harness: it organizes the work needed to turn an informal argument into a coherent Lean repository. Horizon addresses what happens when there are many such runs, many contributors, or many dependent repositories, and the work must continue beyond the lifetime of any one context window.

Horizon does not solve mathematical judgment, guarantee useful decomposition, or remove the cost of coordinating parallel edits. It provides the infrastructure in which those problems can be observed and managed. That distinction matters. Longer-running models make more ambitious formalization possible, but durable state, explicit authority, reviewable history, and human intervention are what make that ambition governable.

The source code and a public dashboard demo are available now.