Summary (Overview)

• This paper reports on an experiment where the AI coding agent Codex successfully autoformalized the computation of $\pi_3(S^2) \cong \mathbb{Z}$ in homotopy type theory using the agda-unimath library in Agda.
• The project ran from June 3 to June 25, 2026, producing 87 literate Agda files and 31,464 lines of code (about 28,000 lines of Agda code), at a cost of approximately $1,750 and 2.08 billion tokens.
• The proof required formalizing several major missing ingredients: the long exact sequence of homotopy groups, the Hopf fibration, join associativity, and the Blakers–Massey theorem (which implies the Freudenthal suspension theorem).
• A key finding was that Codex's success depended heavily on existing human formalizations in the Coq-HoTT library, which Codex effectively translated into the agda-unimath style.
• The authors emphasize the importance of "responsible" autoformalization—producing library-quality code that can be contributed back—and identify significant issues with the Agda MCP server's reliability.

---

Introduction and Theoretical Foundation

Background and Motivation

The experiment was motivated by the lean-eval benchmark released by the Lean Focused Research Organization, which included the problem of proving $\pi_3(S^2) \cong \mathbb{Z}$ in Lean. The authors saw this as an opportunity to test autoformalization capabilities in a different proof assistant—Agda—using the agda-unimath library built on homotopy type theory (HoTT).

The authors note that while Lean is the most popular proof assistant today, other systems have achieved historic successes (e.g., Landau's Grundlagen in Automath, the four-color theorem in Coq, the Kepler conjecture in HOL Light). The key advantage of HoTT is its "synthetic" nature:

"The primitive objects in homotopy type theory—that is, the types—are homotopy types or spaces, and everything definable in homotopy type theory is automatically invariant under homotopy."

Theoretical Foundation: Homotopy Type Theory

In HoTT, the axiom of uniqueness of identity proofs is dropped in favor of the homotopy interpretation where types are spaces, and the identity type $a = b$ represents paths between points $a$ and $b$. Key constructions include:

Iterated loop spaces of a pointed type $(A, a)$:

$$\Omega^{0}(A, a) := (A, a) \qquad \text{and} \qquad \Omega^{n+1}(A, a) := \Omega^{n}(a = a, \mathsf{refl}).$$

Higher inductive types (e.g., the circle $S^1$ generated by a point pt and loop $\text{loop}: \mathrm{pt} = \mathrm{pt}$). The universal property of the circle gives:

$$(S^{1} \to X) \simeq \sum_{x: X} x = x.$$

Suspension: The suspension $\Sigma X$ has two points $\mathsf{n}, \mathsf{s}: \Sigma X$ and a map $\operatorname{merid}: X \to \mathsf{n} = \mathsf{s}$, with the pointed adjunction:

$$(\Sigma A \to_{*} B) \simeq_{*} (A \to_{*} \Omega B).$$

Spheres are defined by iterated suspension: $S^{n+1} := \Sigma^{n} S^{1}$, giving the equivalence $(S^{n} \to_{*} B) \simeq_{*} \Omega^{n} B$.

Homotopy groups are defined as set truncations of iterated loop spaces:

$$\pi_{n}(A) := \left\| \Omega^{n}(A) \right\|_{0}.$$

The Proof Structure for $\pi_3(S^2) \cong \mathbb{Z}$

The calculation has three major ingredients:

1. The long exact sequence of homotopy groups from a fiber sequence $F \to_{*} E \to_{*} B$:

$$\dots \longrightarrow \pi_{n+1}(B) \stackrel{\partial}{\longrightarrow} \pi_{n}(F) \stackrel{i_{*}}{\longrightarrow} \pi_{n}(E) \stackrel{p_{*}}{\longrightarrow} \pi_{n}(B) \stackrel{\partial}{\longrightarrow} \pi_{n-1}(F) \longrightarrow \dots.$$

2. The Hopf fibration $S^{1} \to_{*} S^{3} \to_{*} S^{2}$, constructed via the Hopf construction from the H-space structure on $S^1$. This yields isomorphisms $\pi_2(S^2) \cong \pi_1(S^1)$ and $\pi_3(S^3) \cong \pi_3(S^2)$.

3. The Blakers–Massey theorem (implying the Freudenthal suspension theorem), which gives $\pi_2(S^2) \cong \pi_3(S^3)$.

Combining these, since $\pi_1(S^1) \cong \mathbb{Z}$ and the circle is 1-truncated, one obtains:

$$0 \longrightarrow \pi_{3}(S^{3}) \longrightarrow \pi_{3}(S^{2}) \longrightarrow 0 \longrightarrow 0 \longrightarrow \pi_{2}(S^{2}) \longrightarrow \pi_{1}(S^{1}) \longrightarrow 0,$$

yielding $\pi_3(S^2) \cong \mathbb{Z}$.

---

Methodology

Experimental Design

The authors selected agda-unimath because it already contained definitions of spheres, homotopy groups, group isomorphisms, and the integers—but was missing the major proof ingredients (long exact sequence, Hopf fibration, Freudenthal theorem). They first checked with the community on Discord that no human-led effort was in progress.

Tools and Setup

• Codex (OpenAI's coding agent) was the primary autoformalization tool.
• A Claude Code-generated formalization plan correctly identified a critical indexing subtlety: the agda-unimath concrete-homotopy-group n A names the $(n+1)$-st abstract homotopy group, so $\pi_3(S^2)$ corresponds to concrete-homotopy-group 2 (sphere-Pointed-Type 2), not index 3.
• Skills and reference documents were provided to Codex, covering library conventions, how to search the library, foundational vocabulary, and interpreting Agda error messages.
• A check.sh script ran the actual Agda binary with unsolved metavariables disallowed—the definitive success criterion, since the Agda MCP server was found to sometimes report "ok-complete" on code Agda rejects.

The Formalization Plan

The initial plan identified 35 dependencies, 11 of which were missing, including:

1. Pointed fiber sequences
2. The long exact sequence of homotopy groups
3. The Hopf fibration for connected H-spaces
4. The connected H-space structure on $S^1$
5. The Hopf fibration $S^1 \to_{*} S^3 \to_{*} S^2$
6. The computation $\pi_n S^1 \cong 0$ for $n > 1$
7. The Freudenthal suspension theorem (via Blakers–Massey)
8. The isomorphisms $\pi_{n+3} S^{n+3} \cong \pi_{n+2} S^{n+2}$
9. The computation $\pi_n S^n \cong \mathbb{Z}$ for $n > 1$
10. The final isomorphism $\pi_3(S^2) \cong \mathbb{Z}$

Key Problem-Solving Strategies

• Top-down reasoning: Instructing Codex to decompose the target isomorphism with holes left for later proofs.
• Consulting Coq-HoTT: Directing Codex to use the existing human formalizations in the Coq-HoTT library as guides—this proved crucial for the long exact sequence, join associativity, and Blakers–Massey.
• Persistent prompting: Phrases like "Keep working hard and don't stop until the Blakers Massey theorem is proven" were effective.

---

Empirical Validation / Results

Timeline and Milestones

Metrics

• Code size: 87 literate Agda files, 31,464 lines total (~28,000 lines of Agda code)
• Largest files: Join associativity (7,436 lines—the hardest-fought result) and Blakers–Massey (5,474 lines—completed surprisingly quickly)
• Commits: 151 between June 3 and June 27
• Cost: 2,079,055,195 tokens, $1,750.49 (June 9–27; earlier usage on a free account is unrecoverable)

Key Technical Hurdles

1. Long exact sequence: Codex struggled with exactness at higher stages, attempting multiple constructions of the boundary map $\Omega^{n+1}B \to_{*} \Omega^n F$ with sign convention incompatibilities. Success came from following Coq-HoTT's "hard structural route."

2. Join associativity ($S^1 * S^1 \simeq S^3$): Codex initially pursued "side quests" until redirected. The successful approach, copied from Dan Christensen's Coq-HoTT formalization, used join symmetry around a "twisting" equivalence:

$$(A * B) * C \simeq C * (A * B) \simeq A * (C * B) \simeq A * (B * C).$$

3. Blakers–Massey theorem: Completed in ~7 hours after the prompt "Keep working hard and don't stop until the Blakers Massey theorem is proven," guided primarily by Mike Shulman's Coq-HoTT formalization.

Agda MCP Server Issues

The extraction of MCP calls from session logs revealed:

• 711 total MCP calls, mostly for loading files, inspecting goals, and inferring types
• 290 instances of misleading behavior, including 70 replies reporting success while containing an Agda error
• The root cause: the server conflates three questions—whether the request was processed, whether Agda accepted the command, and whether goals/metavariables remain open

---

Theoretical and Practical Implications

Lessons on Autoformalization

The authors credit success to three factors:

1. agda-unimath's strong infrastructure: Existing background on loop spaces, suspensions, joins, pushouts, truncations, and the computation $\pi_1 S^1 \cong \mathbb{Z}$.

2. A clear natural-language source: [Uni13] (the HoTT Book) provided outlines for the general proofs.

3. Existing human formalizations in Coq-HoTT: This was unanticipated but ultimately decisive. The authors conclude:

"We now believe that success of this experiment was ultimately predicated on the fact that humans have done this before."

Code Translation Capability

A notable finding is Codex's ability to translate formalized code across libraries—from Coq-HoTT to agda-unimath—despite incompatibility issues between formalized mathematics in different systems. This is described as "a major step forward" for the practical problem of library interoperability.

Responsible Autoformalization

The authors emphasize that autoformalization must support, not undermine, human-led efforts:

• They checked with the community before starting to avoid conflicts with human work.
• They distinguish their approach from incidents where autoformalizers "piggybacked upon and then stole credit from a human-led collaboration."
• They consider the project incomplete until library-quality code is contributed back to agda-unimath, acknowledging the raw Codex output is "insufficiently documented, insufficiently explained, and far too verbose."

The Role of the Agda MCP Server

The authors argue that a trustworthy interactive server is essential for human-AI collaboration. A faithful MCP server would give "a human and an agent a shared, machine-checked view of the same unfinished proof, in which either one can leave a hole for the other to attempt"—enabling top-down collaboration where the division of labor is visible in the proof state itself.

---

Conclusion

The experiment demonstrated that Codex can autoformalize a significant mathematical result—$\pi_3(S^2) \cong \mathbb{Z}$—in homotopy type theory with agda-unimath, completing the task in under a month at modest cost. However, the success was heavily dependent on:

• The strong existing infrastructure of agda-unimath
• Clear natural-language proofs in the HoTT Book
• Human-authored formalizations in Coq-HoTT that Codex could translate

Future Directions

1. Improved Agda MCP server: The authors plan to develop a server that distinguishes between request processing, Agda acceptance, and open goals, tested against their catalogued defects.

2. Automated prompting: A driver that hands the agent one module at a time and verifies results independently, removing the dependency on a human prompter's availability.

3. Better AI communication: The authors found AI-generated logs and "risk assessment" language (e.g., "Hopf fibration risk: Constructing the fibration from the H-space circle...") harder to understand than traditional mathematical prose, and suggest coaching models toward more conventional communication.

4. Library contribution: The authors plan to work with agda-unimath maintainers to extract library-quality code through a series of PRs, contributing their own efforts to the refereeing process.

Final Reflection

The experiment highlights both the promise and the current limitations of AI-assisted formalization. While Codex successfully produced a complete proof, the authors are candid that this was "predicated on the fact that humans have done this before"—suggesting that the current state of autoformalization is best characterized as sophisticated code translation rather than independent mathematical discovery. The path forward lies in making AI tools that genuinely support and extend human formalization efforts, with trustworthy interactive feedback and responsible contribution back to the mathematical community's shared libraries.