Summary (Overview)

• MathAtlas is the first large-scale autoformalization benchmark for graduate-level mathematics "in the wild", containing ~52k theorems, definitions, exercises, examples, and proofs extracted from 103 graduate mathematics textbooks.
• The benchmark is enriched with a mathematical dependency graph containing ~178k relations, making it the first autoformalization benchmark to include inter-entity dependency relations, enabling dependency-aware autoformalization systems.
• Extensive experiments show MathAtlas is extremely challenging: strong baselines achieve at most 9.8% correctness on theorem statements and 16.7% on definitions.
• Performance degrades substantially with dependency depth: on MA-Hard (700 entities with deepest dependency trees), the best model achieves only 2.6% correctness.
• The paper also introduces MA-Align, a semantic faithfulness benchmark of 200 entities, showing that prior faithfulness metrics have significant room for improvement on graduate-level mathematics.

---

Introduction and Theoretical Foundation

Background and Motivation

The popularity of formal mathematics (computer-verifiable mathematics) has grown dramatically in recent years. Together with advances in AI, this has spurred interest in autoformalization — the task of automatically converting natural language mathematics to a formal verifiable language such as Lean.

Prior autoformalization work has focused largely on olympiad or undergraduate mathematics (e.g., miniF2F, ProofNet), where:

• Mathematical statements require limited prerequisite material
• Much of the required theory has already been formalized by humans in libraries such as Mathlib

Challenges in Advanced Mathematics

In graduate-level mathematics, autoformalization becomes significantly more complex:

1. Large prerequisite theory: Advanced mathematics has extensive prerequisite material, much of which has yet to be formalized.
2. Dependency synthesis: An autoformalization system must retrieve or produce the necessary dependent theory, correctly formalize it, and then formalize the target statement.
3. Definition formalization gap: Existing benchmarks focus on theorem statements, ignoring formalization of mathematical definitions. Systems that cannot formalize definitions are limited by the level of existing theory.

Key Research Questions

The paper addresses three central questions:

1. How well do current autoformalization systems perform on graduate-level, in-the-wild mathematics?
2. How does dependency depth affect autoformalization performance?
3. Do existing semantic faithfulness metrics generalize to harder domains?

---

Methodology

Dataset Construction Pipeline

The construction of MathAtlas follows a multi-stage pipeline:

1. Collection: 103 PDFs of graduate mathematics textbooks spanning 87 fields and subfields (algebra, analysis, geometry, number theory, probability, quantum theory, category theory, topology, etc.).

2. Conversion: PDFs are converted to MMD (mathematical markdown) files; pages containing metadata (indices, glossaries) are filtered out.

3. Entity Extraction: An entity extraction model identifies spans of text corresponding to entity types (definitions, theorems, proofs, examples, exercises) along with any identifiers (e.g., "Theorem 4.3").

4. Reference Extraction: A reference extractor identifies references to other entities, objects, or local variables within each entity.

5. Name Extraction: On definition entities, a name extraction system identifies the name(s) of the defined object(s).

6. Relation Extraction: A dependency graph is constructed with:

   • "Refers-to" relations between entity references and target entities
   • Relations between object references and the entity defining that object
   • "Proves" relations between proof entities and theorem entities

Entity and Relation Types

Entities are spans of informal text that can be formalized:

• Definitions, theorems, proofs, examples, exercises
• Entities can contain multiple formalizable items (e.g., a definition defining two objects)

References include:

• Entity references: references to other entities (e.g., "Theorem 4.3")
• Object references: references to dependent mathematical objects
• Local variable references: variables not explicitly defined in the entity itself

Dependency metrics:

• Dependency depth: maximum height of an entity's dependency tree
• Dependency mass: total number of unique nodes in an entity's dependency tree

Dataset Statistics

• 52,052 entities: ~18k theorems, ~10k exercises, ~10k definitions, ~10k proofs, ~5k examples
• ~193k object references (avg 3.69 per entity); 83.7% matched to a target entity
• ~17k entity references; 99.8% matched to a target entity
• Average dependency depth: 30 (median 17), ranging from 0 to 80
• Fields like Lie algebra and quantum groups have average depth ~50, while set theory and logic have ~6

Evaluation Metrics

The paper uses a combined metric of compile rate and semantic faithfulness, called correctness:

$$\text{Correctness} = \text{Compile Rate} \times \text{Faithfulness}$$

A formal statement must both compile and be faithful to the informal statement to be considered correct.

MA-Align Construction

MA-Align is a semantic faithfulness benchmark of 200 syntactically correct statements and definitions from MathAtlas. Each informal entity is formalized by gpt-oss-120b and annotated with a binary label ("aligned" or "misaligned").

---

Empirical Validation / Results

Intrinsic Quality Analysis

Entity extraction quality (250 annotated entities, 50 per type):

Relation extraction quality (100 annotated references):

Reference extraction was 96% accurate (errors were identifiers mistaken as entity references or names mistaken as object references).

Autoformalization Results

Statement formalization (theorems, examples, exercises):

Definition formalization:

MA-Hard performance (deepest dependency trees):

Key Findings

1. Disparity between compilation and correctness: Kimina 7B achieves 27.3% compilation but only 2.3% correctness — many formalizations compile but are semantically incorrect.

2. Dependency depth strongly correlates with difficulty: A two-sample Kolmogorov–Smirnov test shows significant difference between max depth distributions for correct vs. incorrect examples (p < 0.001).

3. Mathlib grounding helps: 27.9% of definitions grounded in Mathlib are correctly formalized vs. 16.8% of missing definitions (chi-square p < 0.001).

4. Local context hurts performance: Including 300 tokens of local context decreases performance from 20.3% to 17.4% on definitions and 10.5% to 8.6% on statements for the best model.

Semantic Faithfulness Results (MA-Align)

CriticLean shows strong performance on prior benchmarks but drops notably on MA-Align, while gpt-5.2 with an engineered prompt improves on MA-Align at the cost of performance on prior benchmarks.

---

Theoretical and Practical Implications

Implications for Autoformalization Systems

1. Dependency-aware systems are needed: The strong correlation between dependency depth and failure rate demonstrates that autoformalization systems must be able to retrieve or synthesize prerequisite theory before formalizing target statements.

2. Definition formalization is a distinct challenge: Fine-tuned models trained on theorem formalization fail to generalize to definitions, indicating that definition autoformalization requires specialized approaches.

3. Faithfulness evaluation is unsolved: High performance on prior faithfulness benchmarks (ConsistencyCheck, CriticLeanBench) does not transfer to graduate-level mathematics, suggesting these metrics may be overfit to simpler domains.

4. Mathlib contamination effects: Entities grounded in Mathlib are significantly easier, likely because LLMs have seen Mathlib in training data — this should be accounted for when evaluating autoformalization systems.

Practical Implications

• For benchmark design: MathAtlas provides the first dependency graph for autoformalization, enabling isolated study of components like retrieval or synthesis.
• For model development: The MA-Hard subset provides a focused challenge for advancing dependency-aware systems.
• For evaluation: MA-Align provides a more challenging faithfulness benchmark covering both statements and definitions at the graduate level.

---

Conclusion

Main Takeaways

1. MathAtlas is a challenging, high-quality benchmark: With 90.4% entity extraction quality and 94.8% relation extraction F1, it provides a reliable testbed for graduate-level autoformalization.

2. Current systems perform poorly: The strongest baseline achieves only 9.8% correctness on statements and 16.7% on definitions — far below what would be needed for practical use.

3. Dependency depth is a critical bottleneck: Performance degrades dramatically with dependency depth, with only 2.6% correctness on MA-Hard.

4. Faithfulness evaluation needs improvement: Existing semantic faithfulness metrics show significant performance drops on graduate-level mathematics.

Future Directions

• Dependency-aware autoformalization: Developing systems that can retrieve or synthesize prerequisite theory before formalizing targets.
• Definition formalization: Creating specialized methods for formalizing mathematical definitions, not just theorems.
• Local context integration: Understanding how to effectively incorporate local context without confusing models.
• Research-level mathematics: Extending beyond graduate-level to research mathematics.
• Addressing copyright limitations: The Springer split requires users to have access to the textbooks, potentially limiting reproducibility.

Release

The authors release MathAtlas, MA-Align, and experimental code to support future research in in-the-wild autoformalization. An open split of ~70% of the data (excluding Springer-copyrighted material) is publicly available, with code to generate the full dataset for those with Springer access.