An AI agent tries to formalize a topology textbook, one checked proof at a time

From textbook language to machine-checkable proofs

A textbook might state a theorem in familiar mathematical language, while a Rocq library encodes the same idea using different names, definitions and explicit assumptions. In set theory, even details that a mathematician leaves implicit—such as whether a collection is a set or a proper class—may need to be spelled out. A proof that works on its own must also fit the surrounding library: it should establish the reviewed statement, rely only on allowed assumptions and leave the project building successfully.

Megrez, developed by Tiancheng Xu and Wensheng Yu, is a system for managing this process. It coordinates a general-purpose coding agent with Rocq tools and a library of formalized mathematics. Rocq’s kernel checks proof terms mechanically, but the agent still has to identify a suitable route and express it in the library’s language.

The authors organize Megrez around three problems: matching textbook concepts to library declarations; keeping proof attempts aligned with Rocq’s current goal; and integrating accepted results into a growing codebase. The system’s evaluation centers on MKTopos, a Rocq formalization of a point-set topology textbook over Morse–Kelley set theory.

A map of the library, and short proof attempts

Megrez builds a searchable knowledge graph from Rocq source files, compiler-generated references and curated metadata. The graph links declarations to concepts, textbook items and proof dependencies. It also includes Chinese aliases and groups related declarations into concept clusters, offering routes to relevant results beyond a simple search for matching words.

For a proof, the agent retrieves candidate premises and first writes a mathematical sketch. It then tries tactics in short bursts—between one and five at a time—and inspects the resulting proof state or error. Failed approaches are recorded for the current goal. At set checkpoints, the agent reviews the goal and those failures, then revises its sketch. The ledger is local to the proof: the authors say their early tests found little benefit in carrying detailed proof trajectories from one theorem to another.

Acceptance is deliberately stricter than “the code compiled.” The system checks that the proof establishes the reviewed statement, audits its assumptions and dependencies, and runs a full project build. Human reviewers also check statements before proof work and review semantic annotations added to the knowledge graph. In batches of theorems, the system tracks dependencies and uses saved state to recover from interruptions; source changes that it cannot safely classify are left for human inspection.

What the authors report

The MKTopos corpus contains 3,894 formal declarations, including 2,529 completed proofs, across 262 files. Its knowledge graph includes 60,982 reference edges, most resolved using compiler-generated data. The authors also test retrieval on synthetic graphs scaled to 10,000 and 100,000 nodes. In those tests, the newer full-text search was faster than the older search on the reported interactive workloads; for an exact-identifier query on the 100,000-node graph, the paper reports a change from 72.29 milliseconds to 1.23 milliseconds. These are search measurements, not measures of how often the agent can prove an arbitrary theorem.

Three case studies illustrate how the system was used. In one, it reused an existing library definition for a textbook concept and proved results related to choice and Tukey’s lemma. In another, it reused constructions across chapters to formalize connectedness results for finite and arbitrary products. A third describes work on the two-dimensional Brouwer fixed-point and Jordan separation theorems. These examples show the authors’ workflow in action; they do not by themselves establish that Megrez can formalize textbooks broadly or outperform other systems under a controlled comparison.

What remains uncertain

The paper’s evidence is focused on one library, one proof assistant and one area of mathematics. Its retrieval benchmarks include synthetic data, and the case studies do not provide a broad, independent benchmark of success across textbooks or mathematical domains. The authors also identify practical limitations: curated metadata affects retrieval, compiler references show symbol occurrences rather than minimal logical dependencies, and the system’s safeguards do not replace operating-system sandboxing for untrusted processes.

The distinction between proof checking and mathematical interpretation matters. A kernel can verify that a proof follows from a formal statement and its permitted assumptions; it cannot, by itself, determine whether the formal statement faithfully captures the textbook’s intended claim. That is why Megrez includes human review of statements and annotations.

The source is an arXiv technical report, and the supplied material does not establish that it has undergone peer review. The results are best read as a detailed engineering demonstration of one approach to cumulative formalization—not as a general verdict on AI theorem proving. Its most concrete contribution is a proposed workflow that treats retrieval, feedback, review and project-wide verification as parts of the same task.