1 Introduction↩︎

In recent years, Interactive Theorem Provers (ITPs) such as Coq [1], Isabelle [2] and Lean [3] have become crucial ecosystems for formalized mathematics. Among these, Lean 4, together with its comprehensive library Mathlib [4], is pioneering a new paradigm for formalization. However, the continuous growth of this ecosystem is always constrained by the immense manual effort and the deep expertise that formalization demands. To address this, the research community has turned to Large Language Models (LLMs) for auto-formalization the process of translating informal (or natural language) mathematical statements and proofs into their formal counterparts. While these two processes are interconnected, the accurate formalization of statements is the foundational first step. A correctly formalized statement is a prerequisite for any valid proof and, on its own, is a valuable asset to the mathematical ecosystem, enabling better search, integration, and verification. Thus, despite progress in proof automation [5], [6], the fidelity of this initial statement translation remains a critical bottleneck. LLMs frequently generate formal statements that suffer not only from compilation errors but also from more insidious semantic flaws, a challenge that intensifies when formalizing more complex research or conjecture-level statements.

These foundational shortcomings manifest in several critical downstream failures. An unfaithful translation can derail large-scale data generation pipelines, wasting significant computational budgets on attempts to prove an incorrect premise. For instance, modern provers often decompose complex proofs into smaller, informal lemmas, which are then individually translated and proven. In this workflow, a single flawed translation of a lemma not only invalidates the entire proof structure but can also contaminate the datasets generated during this process, which are crucial for fine-tuning future models. Furthermore, as the research community pushes towards formal models that can autonomously explore conjecture-level problems, the inability to create and utilize the necessary, often unseen, premises (i.e. definitions, lemmas, theorems, etc.) becomes a critical roadblock. Any system lacking this capability is bound to fail at the outset of such ambitious tasks. In this work, we address these challenges by introducing a robust methodology to generate, iterate, and verify formal statements, tackling these foundational bottlenecks through automated structural reasoning.

One primary challenge stems from the static nature and inherent fallibility of an LLM’s pre-trained knowledge. While foundational work has demonstrated the potential of LLMs up to undergraduate mathematics [7], [8], these methods exhibit critical failure modes when confronted with research-level statements, where LLMs are prone to hallucination and outdated pre-trained knowledge. They generate invalid codes with functions either non-existent in Mathlib, or incompatible with rapidly evolving library toolchains. To address this, we integrate a Retrieval-Augmented Generation (RAG) framework, grounding the formalization process by dynamically querying the most current version of the Mathlib library, mitigating the model’s dependence on static knowledge and ensuring compatibility with the evolving toolchain.

Beyond the issue of knowledge retrieval, a more profound challenge lies in synthesis. Research-level mathematics fundamentally involves creating new mathematical objects and definitions, one-pass generation methods, even when augmented with retrieval, fail at this task because they cannot spontaneously synthesize definitions for concepts absent from existing libraries. To address this, we develop an agentic pipeline driven by a Graph-of-Thought (GoT) formalizing process. This approach emulates an expert mathematician’s workflow by recursively decomposing dependencies of definitions until they are well-grounded, then synthesizes their formal statements in a bottom-up order until the primary target is formalized. To ensure the robustness of this process, a compiler-in-the-loop reflection mechanism is employed at each node.

Once a statement is generated and pass the compiler check, the ultimate challenge is to ensure its semantic correctness. While existing methods like LeanScorer [9] have advanced semantic checking by performing fine-grained comparisons, they fail to detect subtle definitive discrepancies between formal and informal terms due to reliance on superficial textual similarity. To overcome this limitation, we introduce AriaScorer, an enhanced semantic checker that incorporates a term-level grounding step. AriaScorer retrieves the authoritative definitions of all Lean terms from Mathlib and injects this formal context into the comparison process, enabling a more rigorous and accurate evaluation.

Equipped with this validated checker, we evaluated Aria’s end-to-end performance on a suite of research-level datasets. We measure final accuracy, which we define as the proportion of the generated formalized statements that pass both compiler and semantic correctness checks. The results demonstrate a significant leap over prior work, with Aria achieving 68.5% on the ProofNet benchmark while also surpassing previous state-of-the-art models on others, including FATE-H (71.0% vs. 43.0%) and FATE-X (44.0% vs. 24.0%). Most notably, on a challenging set of real-world mathematical conjectures where all baseline models score 0%, Aria achieves a 42.9% success rate, demonstrating a unique capability for research-level formalization.

The main contributions of this paper are as follows:

• We introduce Aria, a statement auto-formalizer agent that emulates the human formalization process by integrating retrieval-augmented generation, graph-of-thought planning, and a compiler-guided self-reflection mechanism that is especially effective on conjecture-level problems.

• We develop a term-level grounded semantic scorer, AriaScorer, to detect subtle discrepancies between informal statements and Lean terms, and to accurately verify the mathematical correctness of formalizations.

• We achieve state-of-the-art performance with substantial improvements over previous methods, reaching 68.5% on ProofNet, 71.0% on FATE-H, 44.0% on FATE-X, and 42.9% on real-world conjectures proposed by mathematicians.

The remainder of this paper is structured as follows. Section 2 reviews related work. Section 3 details our proposed methodology, including Aria’s architecture and its core components. Section 4 presents our experimental results and their analysis. Finally, Section 5 concludes the paper.

2 Related Work↩︎

2.0.0.1 Auto-formalization

The rapid advancement of Large Language Models (LLMs) has catalyzed significant progress in auto-formalization. Early efforts demonstrated success by leveraging few-shot in-context learning (ICL) [10]–[12]. As the Lean community grew and its Mathlib library became more comprehensive, the availability of large-scale datasets enabled the development of specialized models through supervised fine-tuning (SFT) [7], [8], [13], [14]. More recently, Reinforcement Learning (RL) has shown potential in mathematics and inference, and several works have leveraged RL training to enhance the quality of auto-formalization [9], [15]. In parallel, other methods have focused on enhancing the quality and reliability of the generation process itself. With the increasingly powerful search capabilities within the Lean ecosystem, Retrieval-Augmented Generation (RAG) has proven effective at providing models with relevant definitions and theorems from the extensive Mathlib library [16]. Concurrently, novel methodologies like Process-Supervised Verification (PSV) leverage direct feedback from compilers to guide the model’s learning process, significantly improving the correctness and reliability of the generated formalizations [17]. Similarly, in the adjacent field of automated theorem proving, recent works [6], [18], [19] have demonstrated the efficacy of reflection mechanisms, enabling systems to iteratively critique and refine their reasoning strategies.

2.0.0.2 Semantic Check

As methods for statement auto-formalization have become more sophisticated and diverse, it is crucial to establish a credible way to evaluate the extent to which the formal statement preserves the mathematical meaning of its informal counterpart. Human experts can certainly provide reliable evaluations of consistency [13], but as statements grow more complex, such evaluations become increasingly demanding. Consequently, perplexity [20] and BLEU [13], [20] have been used as proxy metrics. It is also common to use an LLM to back-translate valid formal statements into informal statements, and then employ another LLM to assess semantic preservation [7], [21], [22]. Additionally, a combined structure of unanimous voting among LLM judges and validation by Lean experts has been introduced, serving as a reward signal during training [8]. Moreover, subtask decomposition of informal statements has been considered, resulting in a more fine-grained filtering of incorrect formalizations [9]. Recently, an automated neuro-symbolic method for determining the mathematical equivalence of two formal statements has been widely adopted. This approach establishes equivalence if and only if a formal proof can connect the two statements, by using semantic-preserving tactics [23], [24].

3 Methodology↩︎

This section details our methodology, which is comprised of two primary components. The overall pipeline is shown in Figure 1. Section 3.1 describes Aria’s architecture, a structured pipeline designed to navigate the deep conceptual dependencies in conjecture-level mathematical statements. Then Section 3.2 presents our integrated semantic checker, which verifies whether the agent’s output is faithful to the original mathematical intent.

3.1 The Graph-of-Thought (GoT) Auto-Formalizer Pipeline↩︎

In this section, we detail the architecture of our agent, Aria. This architecture moves beyond the conventional approach of direct, single-step generation. These methods often fail when applied to complex, conjecture-level statements. As illustrated in Figure 1, our agent operates through a structured pipeline that systematically deconstructs, resolves, synthesizes and verifies a formalization, mirroring the methodical process of a human mathematician.

This pipeline uses a Graph-of-Thought (GoT) planner to deconstruct an informal statement into a conceptual graph, where each concept node represents a definition, structure or class, as illustrated in Figure 1 (A). Each concept node in the graph is then processed by a grounding module, which employs a Retrieval-Augmented Generation (RAG) framework powered by LeanSearch [25] to anchor known concepts to the Mathlib library. For ungrounded concepts, a synthesis module generates new definitions bottom-up, as depicted in Figure 1 (B). All outputs are validated and refined by a compiler-in-the-loop reflection module. Finally, we employ a retrieval-based checker to verify semantic correctness.

3.1.1 GoT Decomposition Phase↩︎

To manage the complex, acyclic dependency graph of definitions and lemmas required to formalize a high difficulty-level statement, our agent’s architecture is centered around a Planning Module based on the GoT paradigm. This module transforms the monolithic task of formalization into a structured, manageable workflow by modeling it as the construction and resolution of a conceptual dependency graph, as shown in Figure 1 (A). This approach is founded on a key principle of mathematical abstraction, which our agent leverages directly: any concept, no matter how complex, can be defined solely in terms of its immediate prerequisite concepts.

The core of our planning module is a conceptual dependency graph, a dynamic data structure that serves as the agent’s working memory. This graph consists of concept nodes and directed edges, where each node represents a mathematical concept required for the final formalization.

For a given statement, Aria initiates a full formalization routine: it performs a top-down dependency expansion of the concept graph until all leaf nodes can be grounded in Mathlib. To achieve this grounding, the agent queries LeanSearch at each node. LeanSearch is a specialized search engine whose index is continuously updated to reflect recent versions of Mathlib, thereby remaining effective as Mathlib evolves. This retrieval process returns a ranked list of candidates from Mathlib, where each candidate consists of a formal statement and its corresponding informal description, ordered by their semantic relevance to the input concept name.

Since the top ranked search result is not always the canonical definition required for formalization, the agent employs an LLM as a sophisticated reasoner to analyze the retrieved candidates, identifying the single best appropriate canonical definition for the concept. If the reasoner concludes that no suitable match exists among the candidates (i.e., the concept is not grounded in Mathlib), the node is treated as an internal node in the dependency graph (as depicted in Figure 1 (A). Its unresolved status triggers the planner to continue the top-down expansion of its children, after which the node is marked for synthesis.

3.1.2 GoT Synthesizing Phase↩︎

Immediately upon completing all expansions, the agent transitions to a bottom-up synthesis phase for the whole graph, which is shown in Figure 1 (B). The synthesis module is invoked for any concept that could not be grounded in the Mathlib library (for instance, the concept "Cohen-Macaulay Module" in Figure 1 (B)). This module is responsible for generating verifiable formal definitions from the ground up, guided by a robust compiler-in-the-loop reflection process that ensures syntactic correctness.

For a given target concept, the agent first collects the verified formal code of all its immediate dependencies (i.e. its children in the dependency graph) to use as context for the LLM to generate a formal Lean definition for the target. The generated code is immediately sent to the Lean compiler for a syntactic check. If compilation fails, the error message along with the failed code is then returned to the LLM as feedback for refinement. If it succeeds, the code is marked as synthesized and used for the synthesis of its parent node.

While this process ensures syntactic validity, it cannot preclude "correctly-typed but semantically wrong" translations. To check the semantic correctness of our code with a more flexible approach, our methodology incorporates an enhanced retrieval-based semantic consistency checker, which is detailed in Section 3.2.

3.2 Semantic Correctness Module: AriaScorer↩︎

3.2.1 Groundwork: LeanScorer↩︎

We propose a semantic correctness checker for auto-formalized Lean statements aimed at mitigating hallucinations and reducing the false positives inherent in LLM-generated outputs. To address the densely packed, assumption-sensitive nature of high difficulty-level statements (such as conjectures), we adopt the subtask decomposition strategy of LeanScorer [9], which evaluates the semantic correctness through subtask-level comparisons.

Given an original informal statement, it is decomposed into atomic assumptions and conclusions by an LLM, and each resulting subtask is then evaluated to determine how well its formal clause matches the corresponding informal one. Subtasks are labeled as Perfectly Match, Minor Inconsistency, or Major Inconsistency, and these labels are aggregated via a fuzzy integral into a final score between \(0\) and \(1\), where \(0\) indicates the presence of a major error and \(1\) reflects perfect alignment across all subtasks. Besides these two cases, the score decays gradually from \(1\) with accumulating minor inconsistencies, capturing the cumulative effect of subtle deviations. A tunable threshold is applied to make binary decisions, balancing tolerance for small deviations against the need to reject semantically incorrect formalizations. Nonetheless, because this method still relies heavily on surface-level textual similarity, it remains vulnerable to semantic mismatches hidden beneath superficially close expressions, which motivates our introduction of a term-grounded evaluation module.

3.2.2 Term-level Semantic Grounding↩︎

To ensure alignment between the evaluation process and the true semantics of formal Lean statements, we introduce a new step: term-level retrieval and interpretation. In this step, we use jixia³, a static analyzer for Lean, which extracts every Lean term referenced in the formal statement and queries the curated informalized Mathlib dataset established in Herald [7] to retrieve each term’s name, kind, type, value, informal name, and informal description. The retrieved term information, together with the original informal and formal statements, the decomposed subtask list, and few-shot examples, is then provided as context to the LLM during the subtask evaluation stage.

This process serves as the foundation for semantic grounding, enabling AriaScorer to reason over the true meanings of formal components rather than their surface syntax. As a result, AriaScorer can identify subtle inconsistencies, such as reversed parameter order or unintended type coercions, all of which are easily missed by purely textual comparison. This step helps prevent common LLM failure modes, including: (i) overlooking implicit preconditions or constraints embedded in Lean term definitions; (ii) misinterpreting Lean definitions by defaulting to their more familiar mathematical counterparts when the two diverge; and (iii) hallucinating incorrect explanations of Lean terms. These error types and how AriaScorer addresses them are discussed in Section 4.3.3, with detailed illustrations provided in the case studies.

By grounding evaluation in the actual semantics of Lean terms, AriaScorer provides more reliable and fine-grained assessments, particularly in cases involving newly introduced or user-defined structures. To validate the impact of this semantic grounding step, we present an ablation study in Section 4.3, showing clear gains in error detection and reductions in false positives.

4 Experiments↩︎

We conduct extensive experiments to evaluate the performance of Aria and AriaScorer. In Section 4.1, we describe the experimental setup of Aria, while Section 4.2 presents the main results. Section 4.3 demonstrates the comprehensive experiment to validate AriaScorer. Finally, we analyze the contributions of key components through ablation studies in Section 4.4.

4.1 Experimental Setup of Aria↩︎

This section outlines the experimental framework for rigorously evaluating Aria’s performance, including the datasets used and the baselines for comparison.

4.1.1 Benchmarks↩︎

To rigorously assess our agent across diverse difficulty levels and problem types, we evaluate it on a suite of benchmarks. Specifically, we use the widely adopted ProofNet [13] to ensure generalizability and comparability with existing work, and the FATE [26] (Formal Algebra Theorem Evaluation) collection together with a dataset of 14 real conjectures to test performance on complex, research-level problems.

ProofNet

To assess generalizability, we use ProofNet, a widely-adopted benchmark of undergraduate-level mathematics. This ensures our agent’s sophisticated architecture is not only effective for complex conjectures but also robust and competitive on standard problems.

FATE-H & FATE-X

The FATE collection tests our agent on advanced mathematics. FATE-H comprises problems from algebra final exams, while FATE-X contains more difficult problems from PhD qualifying exams and research literature. These benchmarks were specifically chosen to evaluate our agent’s capabilities on complex, research-level mathematics.

Homological Conjectures in Commutative Algebra (Conjectures)

Finally, we test Aria on a set of 14 real-world Homological Conjectures [27] in Commutative Algebra, compiled by Melvin Hochster. These conjectures probe deep connections between the homological properties of a commutative Noetherian ring and its structural characteristics. This serves as a direct and challenging testbed of Aria’s ability to formalize active mathematical research problems.

4.1.2 Baseline Models↩︎

To evaluate the efficacy of our agent’s architecture, we compare it against several leading statement auto-formalization models, including a powerful reasoning model Gemini-2.5-Pro [28] and specialized auto-formalizers including Goedel-Formalizer-V2-32B (Goedel-V2) [29], Kimina-Autoformalizer-7B (Kimina) [8] and Herald-translator (Herald) [7].

4.2 Main Results and Analysis↩︎

To evaluate the performance of our model, we conducted comprehensive tests comparing Aria with the baselines on benchmarks detailed in Section 4.1. As shown in Table ¿tbl:tab:main95results?, our agent demonstrates outstanding performance across all evaluations.

As shown in Table ¿tbl:tab:main95results?, Aria demonstrates a significant advantage over all baselines on each benchmark. However, Our GoT and reflection mechanisms require multiple LLM calls for each translation task within Aria. To ensure a fair comparison of efficiency, it is crucial to consider not only the success rate but also the computational cost, for which we use the number of API calls per problem as the primary metric. As Goedel-V2 is the top-performing specialized model at a single pass, with results comparable to the Gemini-2.5-Pro baseline, we select it for a direct comparison of computational budget against Aria. We first determined that Aria requires an average of 17.7 calls per problem on the FATE-X benchmark.

Based on this, we designed a series of experiments for Goedel-V2, ranging from pass@16 to pass@128. As shown in Table ¿tbl:tab:main95results?, while Goedel-V2’s compilation rate scales with the number of calls, its final accuracy remains lower than Aria’s. Aria maintains a higher final accuracy even when compared to Goedel-V2 at pass@128 (using more than 7x calls).

Most importantly, our comparative analysis on the Conjectures dataset reveals why Aria achieves its breakthrough performance. Through comprehensive case study of the generated codes, We identify distinct shortcomings in baseline models: large reasoning models tend to hallucinate incorrect interfaces due to insufficient expert knowledge of Mathlib, while specialized auto-formalizers lack the mathematical reasoning power to manage conjecture-level conceptual dependencies, as evidenced by their tendency to simply replicate training data formats without a true understanding of the underlying mathematical logic. Aria’s architecture, integrating GoT and retrieval module on top of a strong reasoning model, successfully addresses both limitations. We provide case studies of formalized conjectures in Appendix 6 for further illustration.

4.3 Validation of AriaScorer↩︎

4.3.1 Experimental Setup↩︎

We validated our semantic correctness checker against leading alternatives on the FATE-X benchmark. The evaluation used the Aria agent’s syntactically correct, auto-formalized outputs. This benchmark contains complex mathematical statements and advanced definitions, providing a rigorous test of semantic precision.

Ground truth dataset construction

We create an expert-validated ground truth dataset by labeling each formalization as "True" or "False" based on its mathematical fidelity. The annotations are provided by an algebra Ph.D. candidate in pure mathematics and has also contributed to Mathlib, then independently verified by a second expert with the same credentials. We then used this dataset to benchmark the performance of several semantic correctness checkers.

Baselines

We benchmark AriaScorer against several established methods for checking semantic correctness. The first is LeanScorer [9], a method using decomposition and matching, which we re-implemented as its original version is not open-source. Our re-implementation of LeanScorer also serves as a critical ablation study for AriaScorer, representing our full pipeline but without the term-level grounding step. The second is Back Translation [7], [21], a widely-used pipeline that translates a formal statement back to an informal one and uses an LLM to judge the similarity. For a controlled comparison, AriaScorer, LeanScorer, and BackTranslation are all built upon the same base model: Gemini-2.5-Pro. We also evaluate Gemini-2.5-Pro’s performance on this task directly. This comparison framework ensures that AriaScorer’s accuracy improvements can be attributed specifically to our novel term-level analysis, rather than the underlying language model.

Evaluation Metrics

We evaluate performance using binary classification, where formalizations are labeled positive (correct) or negative (flawed). Performance is based on the counts of True Positives (TP), True Negatives (TN), False Negatives (FN), and False Positives (FP). A False Positive, for instance, occurs when a checker incorrectly approves a flawed formalization. These four outcomes are then used to calculate and report accuracy, precision, recall, and F1 score.

4.3.2 Performance of AriaScorer↩︎

2pt

AriaScorer is the top-performing model for semantic correctness checking on Aria’s output from FATE-X. At a threshold of \(\alpha=0\), it achieves the highest accuracy (89.9%), recall (96.2%), and F1 score (93.5%), significantly outperforming all baselines. Its superior precision and recall compared to LeanScorer underscore the benefits of term-level grounding. Increasing the threshold to \(\alpha=0.9\) boosts AriaScorer’s precision to a peak of 95.5%. This demonstrates a key trade-off: a lower threshold is more tolerant of mathematically equivalent forms, maximizing recall, while a higher threshold imposes stricter criteria, minimizing false positives for real-world deployment. In contrast, the Back Translation baseline, which demands an exact textual match, achieves very high precision but suffers from low overall recall. While we adopt the high-precision setting of \(\alpha=0.9\) in all other experiments, the results at \(\alpha=0\) best demonstrate the fundamental advantage of our term-grounded approach.

4.3.3 Key Findings of AriaScorer↩︎

By incorporating term-level grounding, AriaScorer addresses common failure modes in semantic correctness checking. Our ablation study highlights three of its key strengths:

4.3.3.1 Implicit Semantic Inclusion

By retrieving a formal term’s full definition from Mathlib, AriaScorer identifies any implicit preconditions or constraints it contains. This uncovers crucial dependencies for accurate evaluation that purely textual comparisons would overlook. (See Appendix 7.1).

4.3.3.2 Definition Discrepancy Detection

AriaScorer detects subtle discrepancies between a formal term’s precise definition and the informal concept’s intended meaning. By comparing the retrieved Mathlib definition against the original problem’s context, it identifies when a Lean term, though textually similar, carries a different mathematical interpretation. (See Appendix 7.2).

4.3.3.3 Hallucination Suppression via Grounding

AriaScorer suppresses LLM hallucinations by grounding the evaluation process. Before invoking the LLM, it injects the authoritative Mathlib definitions of all formal terms into the prompt. This constrains the model to reason based on verified ground truths, ensuring its output reflects the actual semantics of the formal code. (See Appendix 7.3).

4.4 Summary of Ablation Studies↩︎

We conduct a series of comprehensive ablation studies to quantify the unique contributions of Aria’s core components: the Reflection mechanism, the Graph-of-Thought (GoT) planner, and the Retrieval-Augmented Generation (RAG) module. Our findings, particularly on the challenging Conjectures dataset, demonstrate that all three are indispensable.

• Ablating the Reflection module, caused performance to collapse on both FATE-X and Conjectures, proving its necessity for achieving correct codes.

• Removing the GoT planner cripped the agent’s ability to formalize novel concepts, reducing successful conjectures from 6 to 1. This highlights its critical role in imposing logical structure. Moreover, we found that the impact of ablating the GoT module is more pronounced on more challenging datasets.

• Disabling the RAG module results in a complete 0% success rate on Conjectures, confirming its crucial function in grounding the agent and preventing foundational hallucinations of non-existent concepts.

Detailed procedures and analysis are provided in Appendix 8.

5 Conclusion↩︎

In this paper, we present Aria, a statement auto-formalization agent integrating retrieval-augmented generation, graph-of-thought planning, and self-reflection mechanism. This integrated approach makes Aria the first agent capable of autonomously synthesizing the complex novel definitions required to formalize high difficulty-level mathematical statements such as conjectures. This capability directly addresses a core limitation of prior methods, which fail due to hallucination and logical errors when encountering unseen concepts. Moreover, we presented a novel semantic correctness checker, AriaScorer, that retrieves definitions from Mathlib for term-level grounding, enabling rigorous and reliable verification.

Our comprehensive experimental results demonstrate that our agent achieves leading final accuracy on benchmarks of varying difficulty, from the undergraduate level to conjectures. This success is particularly pronounced on the highly challenging Homological Conjectures dataset, where our agent achieves breakthrough performance.

Given that statement formalization is a critical prerequisite for theorem proving, our successful formalization of conjecture-level statements established a solid foundation for future work on automated mathematical proof at this frontier of research.

Acknowledgements↩︎

This work is supported in part by National Key R&D Program of China grant 2024YFA1014000, Fundamental and Interdisciplinary Disciplines Breakthrough Plan of the Ministry of Education of China (JYB2025XDXM113), the New Cornerstone Investigator Program, and Ubiquant.

Xintao Yu is supported by the "Qiushi Academic-Dongliang" Project of Renmin University of China (No. RUC24OSDL015).

6 Case study for Aria’s Generated Statements↩︎

In this section, we present a qualitative analysis of Aria’s generated statements through several representative case studies to illustrate its strengths and limitations. For each case, we visualize the agent’s conceptual dependency graph as a "blueprint"–a visualization style standard in the Lean community for representing dependencies–to illustrate its planning process. We then present the final formalization and compare it against the outputs generated by the Goedel-V2-Formalizer-32B and Gemini-2.5-Pro model for the same problem.

6.1 Example 1: Koethe’s Conjecture↩︎

Informal Statement

Let \(R\) be a ring. If \(R\) has no non-zero nil ideal (two-sided), then it has no non-zero nil one-sided ideal (neither left nor right).

Aria Generated Statement

import Mathlib

universe u

/-- An ideal `I` is a nil ideal if every element of `I` is nilpotent. -/
def IsNil {R : Type u} [Semiring R] (I : Ideal R) [I.IsTwoSided] : Prop :=
  ∀ x ∈ I, IsNilpotent x

/--
If a ring `R` has no non-zero nil two-sided ideals, then it has no non-zero nil
one-sided ideals (neither left nor right).
-/
theorem no_nil_ideals_implies_no_nil_one_sided_ideals {R : Type u} [Ring R]
    (h : ∀ (I : Ideal R) [I.IsTwoSided], IsNil I → I = ⊥) :
    (∀ (L : Submodule R R), (∀ x ∈ L, IsNilpotent x) → L = ⊥) ∧
    ∀ (J : Submodule (MulOpposite R) R), (∀ x ∈ J, IsNilpotent x) → J = ⊥ :=
  sorry
  

Goedel Generated Statement

import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

theorem statement (R : Type*) [Ring R] :
  (∀ I : Ideal R, I ≠ ⊥ → ∃ x ∈ I, ¬IsNilpotent x) →
    (∀ L : Ideal R, L ≠ ⊥ → ∃ x ∈ L, ¬IsNilpotent x) ∧
      (∀ R : Ideal R, R ≠ ⊥ → ∃ x ∈ R, ¬IsNilpotent x) := by sorry

Gemini Generated Statement

import Mathlib

variable (R : Type*) [Ring R]

def koethe_conjecture : Prop :=
  (∀ (I : Ideal R), IsNil I → I = ⊥) →
  (
    (∀ (J : Submodule R R), IsNil J → J = ⊥) ∧
    (∀ (K : Submodule $\text{\ttfamily R}^{\text{\ttfamily sop}}$ R), IsNil K → K = ⊥)
  )

Analysis

This example clearly reflects the architectural advantages of Aria over both the specialized formalization model like Goedel and a powerful general reasoning model like Gemini.

Among the three outputs, Gemini’s results successfully preserves the original mathematical intent, correctly identifying the need to distinguish between two-sided and one-sided ideals. However, it fails to compile because it hallucinates a non-existent API (IsNil), reflecting a disconnect between its strong high-level reasoning and its knowledge of the library’s API.

In contrast, while Goedel’s output is compilable, it is semantically incorrect. It fails to capture the non-trivial knowledge that one-sided ideals are represented by Submodule R R and Submodule (MulOpposite R) R, and instead formalizes all ideals as Ideal R, which stands only for two-sided ideals, causing the formalization to deviate entirely from the original mathematical intent.

Aria’s formalization is both syntactically and semantically correct. It uses the proper Mathlib types for the different ideals but also achieves good readability and modularity with a prerequisite formal definition for nilpotent ideals (def IsNil). This success highlights the core advantage of Aria’s GoT architecture. Its ability to perform high-level conceptual planning, while strictly grounding the formalization process in Mathlib, allows it to avoid both the API hallucinations of Gemini and the semantic errors of Goedel.

6.2 Example 2: Existence of Balanced Big Cohen–Macaulay Modules Conjecture↩︎

Informal Statement

Let \(R\) be a Noetherian commutative local ring with maximal ideal \(m_R\). There exists a \(R\)-module \(W\) such that \(m_RW ≠ W\) and every system of parameters for \(R\) is a regular sequence on \(W\).

Aria Generated Statement

import Mathlib

/-- A ring `R` is a Noetherian local ring if it is both Noetherian and a local ring. -/
class IsNoetherianLocalRing (R : Type*) [CommRing R]
  extends IsNoetherianRing R, IsLocalRing R : Prop

-- Note: `ringKrullDim` is already defined in Mathlib.

-- Note: `Ideal.IsPrimary` is standard in Mathlib and its definition
-- matches the one provided in the context.

/--
In a Noetherian local ring `R` of Krull dimension `d`, a "system of parameters" is a
sequence of `d` elements `x₁, ..., xₙ` in the maximal ideal `m` such that the ideal
`I = <x₁, ..., xₙ>` generated by these elements is `m`-primary (i.e., it is a primary ideal
whose radical is the maximal ideal `m`).
-/
def IsSystemOfParameters {R : Type*} [CommRing R] [IsNoetherianLocalRing R]
    (d : ℕ) (x : Fin d → R) : Prop :=
  ringKrullDim R = $\uparrow$d 
  (∀ i, x i ∈ LocalRing.maximalIdeal R) ∧
  (let I := Ideal.span (Set.range x);
   I.IsPrimary ∧ I.radical = LocalRing.maximalIdeal R)

/--
Let $R$ be a Noetherian commutative local ring with maximal ideal $m_R$.
There exists a $R$-module $W$ such that $m_RW ≠ W$ and every system of parameters
for $R$ is a regular sequence on $W$.
-/
theorem exists_module_where_system_of_parameters_is_regular_sequence
    (R : Type*) [CommRing R] [IsNoetherianLocalRing R] :
    ∃ (W : Type*) (_ : AddCommGroup W) (_ : Module R W),
      (LocalRing.maximalIdeal R) • ($\top$ : Submodule R W) ≠ $\top$ ∧
      ∀ (d : ℕ) (x : Fin d → R),
        IsSystemOfParameters d x → RingTheory.Sequence.IsRegular W (List.ofFn x) := by
  sorry

Goedel Generated Statement

import Mathlib
import Aesop
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat
theorem statement (R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
  ∃ (W : Type*) [AddCommGroup W] [Module R W],
      (maximalIdeal R : Ideal R) • W ≠ W ∧
          ∀ (s : Set R), s.Finite ∧ Ideal.span s = maximalIdeal R →
                ∀ (f : R → W), (∀ r ∈ s, f r ≠ 0) → LinearIndependent R f := by sorry

Gemini Generated Statement

import Mathlib

open LocalRing

-- The proposition is defined within a `variable` block,
-- which sets the context for the ring R.
variable (R : Type*) [CommRing R] [IsNoetherianRing R] [LocalRing R]

/--
Formalization of the statement:
"There exists an R-module W such that m_R * W ≠ W and every system
 of parameters for R is a regular sequence on W."
-/
def module_with_regular_sop_exists : Prop :=
  -- "There exists an R-module W..."
  ∃ (W : Type*) [AddCommGroup W] [Module R W],
    -- "...such that m_R * W ≠ W..."
    (maximalIdeal R) • ($\top$ : Submodule R W) ≠ $\top$ ∧
    -- "...and every system of parameters for R..."
    ∀ {s : Fin (Ring.Dimension R) → (maximalIdeal R)},
      (IsSystemOfParameters s) →
      -- "...is a regular sequence on W."
      (IsRegularSequence (fun i ↦ (s i : R)) W)

Analysis

This is a more complex conjecture, and the three generated examples once again highlight the poor performance of a specialized model like Goedel in capturing complex mathematical semantics, as well as the knowledge gaps of a general reasoning model like Gemini regarding the Mathlib library.

In this instance, Gemini uses a definition IsSystemOfParameters which does not exist in the library. And for the concept of a regular sequence, which is available in Mathlib (RingTheory.Sequence.Isregular), it used an incorrect interface (IsRegularSequence). Goedel, on the other hand, failed entirely to grasp the concepts of "regular sequence" and "system of parameters", producing a completely erroneous statement.

In contrast, Aria’s Graph-of-Thought (GoT) architecture helped it correctly identify the key concepts. It successfully searched within Mathlib to find RingTheory.Sequence.IsRegular. By leveraging the deconstruct capabilities of GoT, Aria successfully formalize the definition for system of parameters, and ultimately succeeded in formalizing the entire conjecture.

7 Discussion and Case Study for AriaScorer↩︎

By grounding evaluation in retrieved Lean term information, our checker captures the precise semantics of formal statements with greater accuracy, improving both matching and evaluation quality. In the following section, we present examples showing how the three key innovations contribute to the enhanced performance of AriaScorer.

7.1 Implicit Semantic Inclusion↩︎

Informal Statement

Conditions and Conclusions

Formal Statement translated by Aria

import Mathlib

-- To state that the quotient ring is a UFD, Lean must first know it's an integral domain.
-- This requires the ideal to be prime. The error 'unknown constant' indicates that the
-- function name `Ideal.isPrime_iff_isDomain_quotient` used in the previous attempt does not exist.
-- The correct mathlib theorem is `Ideal.Quotient.isDomain_iff_prime`, which states
-- `IsDomain (R $\big/$ I) $\leftrightarrow$ I.IsPrime`. To prove the `IsDomain` instance from the primality of the
-- ideal, we need the reverse direction of this equivalence, which is accessed with `.mpr`.

-- The `noncomputable` keyword is required because types like `MvPolynomial` over `$\mathbb{C}$`
-- are defined using classical logic and do not have an executable implementation.
noncomputable def kleinianSingularityIdeal : Ideal (MvPolynomial (Fin 3) $\mathbb{C}$) :=
  Ideal.span {
    (MvPolynomial.X 0 : MvPolynomial (Fin 3) $\mathbb{C}$)^2 +
    (MvPolynomial.X 1)^3 +
    (MvPolynomial.X 2)^7
  }

-- We define an abbreviation for the quotient ring type for clarity.
abbrev CxyzModKleinian := MvPolynomial (Fin 3) $\mathbb{C}$ $\big/$ kleinianSingularityIdeal

-- We manually provide the `IsDomain` instance for our quotient ring. Its proof follows
-- from the fact that the ideal is prime, a non-trivial result which we assume with `sorry`.
local instance : IsDomain CxyzModKleinian :=
  (Ideal.Quotient.isDomain_iff_prime kleinianSingularityIdeal).mpr sorry

theorem isUFD_of_C_xyz_mod_x2_y3_z7 :
  UniqueFactorizationMonoid CxyzModKleinian := by
  sorry

Retrieved Lean Terms

{'name': ['MvPolynomial'], 'kind': 'definition', 'value': 'Type u_1 → (R : Type u_2) → [inst : CommSemiring R] → Type (max u_1 u_2)', 'informal_name': 'Multivariate polynomials over $R$ with variables in $\sigma$', 'informal_description': 'The type of multivariate polynomials over a commutative semiring $R$ with variables indexed by a type $\sigma$. Each polynomial is a finite formal linear combination of monomials, where a monomial is a product of variables $X_i$ for $i \in \sigma$ raised to non-negative integer powers, with coefficients in $R$.'}
{'name': ['Ideal', 'span'], 'kind': 'definition', 'value': '{$\alpha$ : Type u} → [inst : Semiring $\alpha$] → Set $\alpha$ → Ideal $\alpha$', 'informal_name': 'Ideal generated by a subset', 'informal_description': 'Given a subset $s$ of a semiring $\alpha$, the ideal $\text{span}(s)$ is the smallest ideal of $\alpha$ containing $s$, defined as the intersection of all ideals containing $s$.'}

Matching And Assessment by AriaScorer

Analysis

In this case, the informal statement asserts that the quotient ring \(R = \mathbb{C}[x, y, z]/(x^2 + y^3 + z^7)\) is a Unique Factorization Domain (UFD), which requires \(R\) to be an integral domain by definition. AriaScorer, empowered by term-level retrieval, correctly accesses the definitions of relevant Lean terms and tracks newly written local instances. This allows it to recognize that the concept of UFD is semantically realized through the combination of IsDomain and UniqueFactorizationMonoid, even though they appear separately in the formal code.

Without this term-level semantic grounding, a checker may mistakenly treat the newly defined local instance as a nontrivial addition to the conclusion, rather than recognizing it as a prerequisite implicitly embedded in the definition of UniqueFactorizationMonoid. By contrast, AriaScorer uncovers this internal dependency and correctly matches the formalization. This case illustrates the strength of semantic grounding: it enables the checker to move beyond surface forms and reason about the structural meaning and interrelation of formal terms—something that purely textual comparison would fail to capture.

7.2 Definition Discrepancy Detection↩︎

Informal Statement

Conditions and Conclusions

Formal Statement translated by Aria

import Mathlib

theorem quaternion_algebra_over_reals_isomorphic_to_hamiltonians_or_matrices
    (A B : $\mathbb{Q}$) (hA : A ≠ 0) (hB : B ≠ 0) :
    Nonempty (QuaternionAlgebra $\mathbb{R}$ (A : $\mathbb{R}$) (B : $\mathbb{R}$) 1 $\cong_{\text{a}}$[$\mathbb{R}$] (QuaternionAlgebra $\mathbb{R}$ (-1) (-1) 1)) $\lor$
    Nonempty (QuaternionAlgebra $\mathbb{R}$ (A : $\mathbb{R}$) (B : $\mathbb{R}$) 1 $\cong_{\text{a}}$[$\mathbb{R}$] Matrix (Fin 2) (Fin 2) $\mathbb{R}$) := by
  sorry

Retrieved Lean Terms

{'name': ['Matrix'], 'kind': 'definition', 'value': "Type u → Type u' → Type v → Type (max u u' v)", 'informal_name': 'Matrix', 'informal_description': 'The type of matrices with rows indexed by a type $m$, columns indexed by a type $n$, and entries in a type $\alpha$. A matrix $M$ can be represented as a function $M : m \to n \to \alpha$, where $M(i,j)$ gives the entry in row $i$ and column $j$.'}
{'name': ['QuaternionAlgebra'], 'kind': 'structure', 'value': '(R : Type u_1) → R → R → R → Type u_1', 'informal_name': 'Quaternion Algebra', 'informal_description': 'The structure representing a quaternion algebra over a commutative ring $R$ with fixed coefficients $a, b, c$, where the elements are of the form $x + yi + zj + wk$ with $x, y, z, w \in R$ and the multiplication rules are determined by $i^2 = a + bi$ and $j^2 = c$. The structure has four components: the real part `re` and three imaginary parts `imI`, `imJ`, `imK`.'}

Matching And Assessment by Aria’s Semanctic Checker

Analysis

In this case, the informal statement introduces \(D_{A, B, \mathbb{R}}\) with multiplication rules: \(\boldsymbol{i}^2 = A\), \(\boldsymbol{j}^2 = B\), and \(\boldsymbol{i}\boldsymbol{j}= -\boldsymbol{j}\boldsymbol{i} = \boldsymbol{k}\). However, the corresponding Lean term actually has completely different rules:\(\boldsymbol{i}^2=A+B\boldsymbol{i}, \boldsymbol{j}^2=1\). These differences are not perceptible by surface text comparison, Both the informal and formal version use \(A\) and \(B\), and have similar algebra structure. By term-level grounding, AriaChecker gets the explicit retrieval of the definition of QuaternionAlgebra, making the semantic incorrectness obvious to AriaScorer. While LeanScorer is deceived by apparent textual similarity and misjudges this case, AriaScorer correctly flags it as "Major Inconsistency". This demonstrates that Defintion Discrepancy Detection enables AriaScorer to distinguish semantic incorrectness, ensuring that the formal statement aligns with the formal statement in mathematical intent.

7.3 Hallucination Suppression via Grounding↩︎

Informal Statement

Conditions and Conclusions

Formal Statement translated by Aria

import Mathlib

open Polynomial

/--
Let $\alpha = \sqrt{(2+\sqrt{2})(3+\sqrt{3})}$. The field $E = \mathbb{Q}(\alpha)$ is a Galois
extension of $\mathbb{Q}$, and its Galois group is isomorphic to the quaternion group $Q_8$.
...    Nonempty (P.Gal $\cong^{\text{*}}$ QuaternionGroup 1) :=
  sorry

Retrieved Lean Terms

{'name': ['IntermediateField', 'adjoin'], 'kind': 'definition', 'value': '(F : Type u_1) →\n  [inst : Field F] → {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → Set E → IntermediateField F E', 'informal_name': 'Field adjunction of a set $ S $ to $ F $', 'informal_description': 'Given a field extension $ E $ of $ F $ and a subset $ S \subseteq E $, the structure `IntermediateField.adjoin F S` represents the intermediate field obtained by adjoining the elements hedral group; when $n=1$, it is isomorphic to a cyclic group of order 4.'}
{'name': ['Polynomial'], 'kind': 'structure', 'value': '(R : Type u_1) → [inst : Semiring R] → Type u_1', 'informal_name': 'Univariate polynomials over a semiring', 'informal_description': 'The structure `Polynomial R` represents the type of univariate polynomials over a semiring `R`, denoted as `R[X]`. Polynomials are constructed using the variable `X` and constant embedding `C` from `R`, forming a semiring structure.'}

Matching And Assessment by Aria’s Semantic Checker

Misjudgment when term-level grounding is eliminated

Analysis

In this case, the Lean statement claims an isomorphism Nonempty (P.Gal ≃* QuaternionGroup 1), using the key Lean term QuaternionGroup 1. It is easily to assume that QuaternionGroup 1 refers to the quaternion group of order 8, \(Q_8\). Actually, QuaternionGroup 1 is isomorphic to the cyclic group \(C_4\), while the actual representation of \(Q_8\) is QuaternionGroup 2. This subtle but important distinction is overlooked when LLM gives the checking purely on surface texts. In the setting without the information of Lean terms, checker is misled by the hallucination of LLM and gives a wrong judgment. In comparison, AriaScorer grounds the checking pipeline in concrete semantics. With the usage of the definition of QuaternionGroup n, AriaScorer correctly flags the statement as "Major Inconsistency", which is in line with human annotation. It gives an example of how the process of hallucination suppression constrains the LLM’s reasoning within Lean terms, guarantees precision in the semantic correctness checking.

7.4 Verification Strategy and Error Propagation Analysis↩︎

7.4.1 Verification Strategy↩︎

A critical architectural decision in our system is the application of AriaScorer exclusively as a terminal evaluator rather than an iterative feedback signal. This design is driven by a strategic trade-off between verification rigor, algorithmic stability, and computational efficiency. AriaScorer is engineered to function as a rigorous, independent checker involving multiple LLM calls and database searches. Consequently, it is computationally expensive and best suited for validating the quality of the completed solution.

Our preliminary experiments with iterative semantic feedback revealed two primary challenges:

• Instability: Correcting semantic issues at intermediate steps frequently disrupted the syntactic structure of the proof, leading to oscillatory behavior where the system toggled between semantic and syntactic errors.

• Inference Efficiency: Given the computational intensity of AriaScorer, applying it to every intermediate node would drastically increase the total inference time. This inefficiency is further compounded by the aforementioned oscillatory behavior.

Furthermore, utilizing AriaScorer as a feedback signal for reflection-in addition to its role as the final checker-introduces a risk of self-referential bias, where the formalizer might learn to overfit the scorer’s specific preferences rather than producing universally correct proofs.

7.4.2 Analysis of Semantic Error Propagation↩︎

We specifically investigated the risk of semantic error propagation, where an incorrect intermediate definition might lead to a finalized but flawed proof. Our empirical data suggests that errors caused by "correctly typed but semantically wrong" intermediate definitions are statistically rare. A root cause analysis of failure cases in the FATE-X dataset revealed that only a single instance of failure was attributable to a flaw in definition synthesis that propagated to cause a final semantic inconsistency.

7.4.2.1 Case Study: The Catenary Ring

To demonstrate the rigor of AriaScorer in detecting such rare propagation cases, we present a detailed analysis of the "Catenary Ring" instance. In this case, the generator synthesized a definition for CatenaryRing that was syntactically valid but mathematically overly restrictive compared to the standard definition.

import Mathlib

universe u

/--
A ring `R` is a catenary ring if it is a commutative Noetherian ring, and for any two
prime ideals `p` and `q` with `p $\subset$ q`, all saturated chains of prime ideals between
`p` and `q` have the same length.

The length of a finite chain of prime ideals `p$_0$ $\subset$ p₁ $\subset$ ... $\subset$ pₙ` is `n`. This corresponds
to the chain having `n+1` elements. Thus, two chains have the same length if and only
if they have the same number of elements (cardinality).
-/
class CatenaryRing (R : Type u) [CommRing R] extends IsNoetherianRing R : Prop where
  /--
  For any two prime ideals `p, q` with `p $≤$ q`, all saturated (i.e. maximal) chains
  of prime ideals in the interval `Set.Icc p q` have the same cardinality.
  -/
  eq_saturated_chain_length :
    ∀ (p q : PrimeSpectrum R), p ≤ q →
      ∀ (c₁ c₂ : Set (Set.Icc p q)),
        IsMaxChain ($\cdot$ ≤ $\cdot$) c₁ →
        IsMaxChain ($\cdot$ ≤ $\cdot$) c₂ →
        Set.ncard c₁ = Set.ncard c₂

/--
A Noetherian Unique Factorization Domain of Krull dimension at most 3 is catenary.
-/
theorem ufd_of_dim_le_three_is_catenary (A : Type u)
    [CommRing A] [IsDomain A] [IsNoetherianRing A] [UniqueFactorizationMonoid A]
    (h_dim : Order.krullDim (PrimeSpectrum A) ≤ 3) :
    CatenaryRing A :=
  sorry

Below is the analysis of AriaScorer:

**A is a catenary ring**:
- Math: $A$ is a catenary ring, i.e., for any two prime ideals $P, Q$ of $A$ with $P \subseteq Q$, any two saturated chains of prime ideals between $P$ and $Q$ have the same length.
- Lean: `CatenaryRing A`. The provided `class CatenaryRing` definition `extends IsNoetherianRing R`, which means that to be a `CatenaryRing`, a ring must be Noetherian in addition to satisfying the chain condition. The mathematical definition provided does not require the ring to be Noetherian. This makes the Lean conclusion stronger than the mathematical one.
- Match: Major inconsistency.

Even though the specific problem context (Theorem ufd_of_dim_le_three_is_catenary) explicitly included the Noetherian ring condition ([IsNoetherianRing A]), AriaScorer correctly identified that the definition itself hallucinated an unnecessary inheritance (extends IsNoetherianRing). This demonstrates that AriaScorer maintains rigorous judgment even when the propagated error is subtle and contextually masked.

7.4.3 Future Outlook↩︎

While the current dependency graphs in FATE-X are relatively shallow (averaging 2-3 layers), minimizing the impact of error propagation, this challenge may become more pronounced in large-scale formalization tasks, such as formalizing entire textbooks. Future work may aim to efficiently integrate semantic signals into larger systems by adopting strategic checkpointing (e.g., verifying every \(k\) layers) to balance efficiency and correctness.

7.5 Limitations of Syntactic Metrics in Research-Level Mathematics↩︎

A potential concern in using a LLM-based evaluator is the risk of self-referential bias. We address this by adhering to a strict architectural decoupling: AriaScorer is utilized solely as a post-hoc evaluator and is never exposed to the agent during generation or reflection. This ensures that the observed performance gains reflect genuine capabilities rather than optimization towards the metric. Furthermore, the reliability of AriaScorer has been validated against human expert annotations on the FATE-X and Conjecture datasets, achieving a 95.5% alignment rate.

7.5.1 Why Syntactic Metrics Are Limited.↩︎

While syntactic metrics such as BEq or simple type-checking are standard for simple formalization tasks, we find them ill-suited for research-level mathematics. At this level, proving logical equivalence between a synthesized definition and a reference statement is often non-trivial. Standard syntactic matchers frequently generate false negatives due to several intrinsic complexities of formal libraries:

1. Multiple Mathematical Definitions: A single concept often has multiple equivalent mathematical definitions. Different contexts (or authors) may prefer different formulations, leading to distinct structures or type classes in Lean.

2. Bundled Type Classes: Structures can be "bundled" differently. For example, a two-variable polynomial ring can be formalized as MvPolynomial (Fin 2) R or Polynomial (Polynomial R). These are not definitionally equal; proving their equivalence requires constructing a complex algebraic isomorphism (\(\simeq_a\)[R]).

3. Inheritance Structures (Diamonds): Type classes inherit from others. Different inheritance paths can lead to "diamond" problems where the formal representations diverge despite representing the same object. This issue is acute in our framework: the Graph of Thoughts (GoT) planner synthesizes deeply structured, multi-layer definition chains. This structured approach naturally induces diamond patterns.

7.5.2 Case Study: The E8 Kleinian Singularity.↩︎

To illustrate why syntactic metrics fail in this domain, we present a specific case from the FATE-X dataset regarding the E8 Kleinian Singularity.

--Aria Generated Code:
import Mathlib
noncomputable def kleinian_singularity_E8_polynomial : MvPolynomial (Fin 3) $\mathbb{C}$ :=
  (MvPolynomial.X 0) ^ 2 + (MvPolynomial.X 1) ^ 3 + (MvPolynomial.X 2) ^ 7
abbrev E8_singularity_quotient_ring :=
  (MvPolynomial (Fin 3) $\mathbb{C}$) ⧸ (Ideal.span {kleinian_singularity_E8_polynomial})
instance kleinian_singularity_E8_ideal_isPrime :
  (Ideal.span {kleinian_singularity_E8_polynomial}).IsPrime := by sorry
theorem isUFD_E8_singularity_quotient_ring :
  UniqueFactorizationMonoid E8_singularity_quotient_ring := by sorry

--Reference Code:
import Mathlib
/--
The ring $R = \mathbb{C}[x, y, z] / (x^2 + y^3 + z^7)$.
-/
abbrev R : Type := (MvPolynomial (Fin 3) \mathbb{C}) ⧸ Ideal.span {(.X 0 ^ 2 + .X 1 ^ 3 + .X 2 ^ 7 : MvPolynomial (Fin 3) \mathbb{C})}
/--
$\mathbb{C}[x, y, z] / (x^2 + y^3 + z^7)$ is a UFD.
-/
theorem quotient_not_UFD :
  ∃ (h : IsDomain R),
    (UniqueFactorizationMonoid R) := by sorry

Both theorems assert the same fact: the coordinate ring of the E8 singularity is a Unique Factorization Domain (UFD).

To formally prove that these two statements are equivalent in Lean (and thus satisfy a strict checker, e.g. BEq), one would need to perform three non-trivial steps:

• Ring Identification: Prove R = E8_singularity_quotient_ring. This requires unfolding the definitions, returning to the quotient construction, and applying rewrite tactics.

• Domain Verification: Prove that R is an integral domain. This follows from the kleinian_singularity_E8_ideal_isPrime instance, but requires a non-trivial proof step.

• Logical Elimination: Prove the lemma (∃ (h : IsDomain R), UniqueFactorizationMonoid R)\(\leftrightarrow\)UniqueFactorizationMonoid R. This involves existential elimination logic.

Bridging this gap requires unfolding 4-5 technical layers and employing intermediate-level Lean tactics. BEq, which operates on structural equality, cannot perform this semantic reasoning. Consequently, we maintain that AriaScorer represents a necessary, reliable, and unbiased standard for this domain.

8 Ablation Studies↩︎

To quantify the individual contributions of the core components within our Aria agent, we conducted a series of comprehensive ablation studies. We systematically disabled the Reflection, Graph-of-Thought (GoT), and Retrieval-Augmented Generation (RAG) modules to measure their impact on the performance. All experiments were conducted on the challenging benchmarks FATE-X and homological conjectures, with the results presented in Table 2 and Table 3.

8.1 Ablating the Reflection Mechanism↩︎

This study is designed to quantify the contribution of our agent’s core iterative self-correction mechanism. In the full Aria agent, each generation step (for both prerequisite definitions and the final theorem) is embedded in a refinement loop that allows for 16 reflection attempts. Within this loop, the agent generates a candidate formal definition or statement and receives feedback from the compiler, and uses this feedback to inform the next generation attempt.

For ablation, we disable the refinement loop entirely, restricting the agent to a single generation attempt at each stage.

As shown in Table 3, ablating the reflection module causes the final accuracy on FATE-X to drop from 44% to 14% and the compilation success rate from 69% to 19%, even lower than that of baseline. This dramatic performance decrease is also observed on the Conjectures dataset, where the success rate plummet from 42.9% to 0%. The result indicates that a single generation is often insufficient for both capturing the semantic nuances and the syntactic rigor of complex mathematical statements. Therefore, we conclude that the Reflection module is a crucial part in our agent’s architecture.

8.2 Ablating the GoT planner↩︎

The experimental setup for this ablation is as follows: first, we extract a flat list of conceptual keywords from the original informal statement. Then, for each concept in this list, we use LeanSearch to retrieve it in Mathlib. In contrast to the full system, this process does not perform any further recursive decomposition, regardless of the search outcome. The agent then directly synthesizes the final formal statement only using the results from this search.

8.2.0.1 Quantitative Analysis.

As shown in Table 2, the impact of GoT scales with problem difficulty. On the challenging Conjectures dataset, the full Aria system successfully formalized 6 of the 14 conjectures, whereas the version without GoT only managed 1. Similarly, on the FATE-X benchmark (Table 3), removing GoT causes the final accuracy to drop from 44.0% to 38.0%, although the compilation success rate remains constant at 69.0%.

However, Table 4 reveals a counter-intuitive phenomenon on the simpler FATE-H dataset: the ablated agent achieves a higher compilation success rate (95% vs. 89%) but a significantly lower final accuracy (54% vs. 71%).

8.2.0.2 The Trade-off between Syntactic Risk and Semantic Rigor.

We attribute the "high compilation, low accuracy" anomaly on FATE-H to a strategic trade-off. The GoT planner prioritizes semantic explicitness by forcing the generation of all necessary intermediate definitions (e.g., explicitly defining extended fields or tensor products as separate structures). While this ensures semantic consistency, it significantly increases the total attack surface for syntactic errors. For instance, the modular style introduces complexities in global namespace management and Lean’s type class resolution-where instances of equivalent but distinct definitions often fail to interoperate without explicit equivalence proofs.

On simpler problems like those in FATE-H, which typically require no prerequisite definitions, this structural overhead yields a net negative impact on compilation. The ablated model, which tends to generate monolithic statement using local let bindings, avoids these interface complexities but fails to capture the correct semantics, leading to lower final accuracy.

8.2.0.3 Scaling to Complexity

This relationship shifts as problem complexity increases. On FATE-X and Conjectures, the "syntactic cost" of longer code is effectively offset by the "structural benefit" of decomposition. Without GoT, the agent’s attempt to formalize novel, high-level concepts monolithically leads to 2 distinct failure modes: synthesis failure (inability to generate complex and definitions) and interface hallucination.

In summary, GoT acts as an indispensable engine for the creative mathematical construction demanded by research-level auto-formalization. Unlike prior works that rely solely on static library retrieval, GoT explicitly leverages the reasoning LLM’s natural-language mathematical capability to construct dynamic dependency graphs. This enables a modular formalization style that bridges the gap between the model’s internal knowledge and the rigorous requirements of the formal system.

8.3 Ablating the RAG module↩︎

To measure the value of Retrieval-Augmented Generation (RAG), we designed this study to contrast live, tool-based retrieval against reliance on the pretrained, static knowledge of the Large Language Model (LLM).

In the full system, the agent’s grounding process is executed by leveraging LeanSearch. The LLM’s task is confined to reasoning over this verified set of options. For the ablated version, we disable the retrieval tool entirely. Instead, the agent directly queries the LLM, to recall the correct formal name for a concept based on its own knowledge.

Our ablation studies, presented in Table 2 and Table 3, reveal the crucial role of the RAG module, particularly as problem complexity increases. While the ablation version resulted in only a moderate drop in final accuracy on FATE-X (from 69% to 61%), its effect on the more challenging Conjectures dataset was absolute, with the success rate collapsing from 42.9% to 0%.

This divergence highlights a key insight into the agent’s capabilities. For moderately complex tasks like those in FATE-X, the agent can partially compensate for the lack of retrieval through its powerful self-reflection mechanism. By interpreting the compiler’s precise feedback on "unknown identifiers," the agent may iteratively rediscover correct Mathlib definitions. However, this trial-and-error recovery process is insufficient for complex conjectures. The 0% accuracy reveals that without the contextual grounding from RAG, the LLM’s inaccurate internal knowledge of Mathlib leads it to hallucinate non-existent definitions and confidently judge them as grounded. This foundational error prevents the generation of compilable code, demonstrating that our RAG module is essential for success on challenging mathematical reasoning tasks.

9 Prompts↩︎

For clarity and reproducibility, we present the prompt frameworks used by Aria across various stages.

10 Generalization Across Mathematical Domains↩︎

While our primary experimental analysis centers on the FATE algebra datasets, the mechanisms underlying Aria are not intrinsically limited to algebra. In this section, we analyze the system’s performance across diverse mathematical fields and discuss the rationale behind our domain selection.

10.1 Performance on Proofnet↩︎

To empirically validate domain generalization, we break down the performance on the ProofNet benchmark by subfield. As shown in Table 5, Aria demonstrates high consistency across undergraduate-level algebra, analysis, number theory and topology. Furthermore, it surpasses the strong baseline (Goedel-V2) in every category. Notably, in number theory and topology, Aria achieves a significant margin in final accuracy, suggesting that its retrieval and planning capabilities are robust to domain shifts.

10.2 Case Study: Borel’s Conjecture in Topology↩︎

Furthermore, we successfully applied Aria to formalize Borel’s Conjecture in topology. This task requires handling distinct mathematical structures (e.g., Manifold, ChartedSpace, HomotopyGroup) that differ significantly from algebraic rings and modules.

This successful formalization confirms that Aria’s GoT planner can effectively navigate the definition dependencies in non-algebraic domains, provided that the underlying library support exists.

import Mathlib

/-- A closed manifold is a compact manifold with empty boundary. -/
class IsClosedManifold {$\Bbbk$ : Type*} [NontriviallyNormedField $\Bbbk$] {E : Type*}
  [NormedAddCommGroup E] [NormedSpace $\Bbbk$ E] {H : Type*} [TopologicalSpace H]
  (I : ModelWithCorners $\Bbbk$ E H) (n : WithTop ℕ∞) (M : Type*) [TopologicalSpace M]
  [ChartedSpace H M] extends IsManifold I n M, CompactSpace M : Prop where
  /-- The boundary of a closed manifold is empty. -/
  boundaryless : {x : M | I.IsBoundaryPoint (chartAt H x x)} = $\emptyset$


/-- An aspherical topological manifold is a topological manifold `M` that is path-connected and for which the `k`-th homotopy group `$\pi_k(M, x)$` is trivial for all `k ≥ 2` and all basepoints `x : M`. -/
structure IsAsphericalTopologicalManifold
    {$\Bbbk$ : Type*} [NontriviallyNormedField $\Bbbk$]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace $\Bbbk$ E]
    {H : Type*} [TopologicalSpace H] (I : ModelWithCorners $\Bbbk$ E H)
    (n : WithTop ℕ∞) (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : Prop where
  /-- An aspherical topological manifold is a topological manifold. -/
  is_manifold : IsManifold I n M
  /-- An aspherical topological manifold is path-connected. -/
  path_connected : PathConnectedSpace M
  /-- The `k`-th homotopy group of an aspherical topological manifold is trivial for `k ≥ 2`. -/
  homotopy_groups_trivial (k : ℕ) (hk : 2 ≤ k) (x : M) :
    Subsingleton (HomotopyGroup (Fin k) M x)


/-- Let $M$ and $N$ be closed and aspherical topological manifolds. If $f \colon M \to N$ is a homotopy equivalence, then $f$ is homotopic to a homeomorphism. -/
theorem borel_conjecture_for_topological_manifolds
    {$\Bbbk$ : Type*} [NontriviallyNormedField $\Bbbk$]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace $\Bbbk$ E]
    {H : Type*} [TopologicalSpace H]
    {I : ModelWithCorners $\Bbbk$ E H}
    {n : WithTop ℕ∞}
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
    [IsClosedManifold I n M]
    (hM_aspherical : IsAsphericalTopologicalManifold I n M)
    {N : Type*} [TopologicalSpace N] [ChartedSpace H N]
    [IsClosedManifold I n N]
    (hN_aspherical : IsAsphericalTopologicalManifold I n N)
    (f : ContinuousMap.HomotopyEquiv M N) :
    ∃ (g : M $\simeq_t$ N), ContinuousMap.Homotopic f.toFun (g : C(M, N)) := by
  sorry

11 Statement on the Use of Large Language Models (LLMs)↩︎

In accordance with the policy, we disclose that Large Language Models (LLMs) played a significant role in the preparation of this manuscript. The authors take full responsibility for all content, including any text generated by these models, and have meticulously reviewed and edited all outputs for accuracy, originality, and scientific integrity.

We utilized Google’s Gemini-2.5-Pro as a language editing tool. Its role was strictly limited to improving clarity, correcting grammatical errors, and rephrasing sentences.

References↩︎