FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels

The paper introduces FATE, a new formal algebra benchmark series spanning from undergraduate exercises to PhD-level research problems, which reveals that current state-of-the-art LLMs struggle significantly with formalizing advanced mathematical reasoning, achieving near-zero accuracy on the most difficult tasks despite stronger natural-language performance.

The Gist

Imagine you are teaching a brilliant, super-fast robot how to do math.

For a long time, we've tested these robots on math competitions (like the International Math Olympiad). Think of these competitions like sprint races. They are short, intense, and require clever tricks to solve specific puzzles quickly. The robots have gotten really good at these sprints; they can run circles around human high schoolers.

But here's the problem: Real mathematical research isn't a sprint. It's more like exploring a vast, unmapped jungle. It requires deep, slow thinking, building new tools from scratch, and understanding complex systems that no one has ever seen before.

The paper you're asking about, FATE, is a new set of "jungle maps" designed to test if robots can actually do this deep, research-level thinking.

The Three Levels of the Jungle (The Benchmarks)

The authors created a series of tests called FATE (Formal Algebra Theorem Evaluation) with three difficulty levels, like climbing a mountain:

1. FATE-M (The Base Camp): These are like textbook exercises. "Here is a rule; apply it to solve this." Most robots can handle this.
2. FATE-H (The High Camp): These are like graduate school exams. You need to combine several rules and think creatively. This is where the robots start to stumble.
3. FATE-X (The Summit): These are PhD-level problems. They are so hard that they often require inventing new definitions and concepts that don't exist in the robot's training manual yet. No robot has successfully climbed this peak yet.

The Big Discovery: The "Translator" Problem

The researchers found something very surprising about how these robots think. They noticed a two-step process:

1. Step 1: The "Chat" (Natural Language): The robot first writes out a solution in plain English, like a human mathematician scribbling on a whiteboard.
2. Step 2: The "Code" (Formal Language): The robot then tries to translate that English scribble into strict computer code (called Lean) that a computer can verify as 100% correct.

The Analogy:
Imagine the robot is a genius architect who can design a beautiful, complex house in their head and draw it on a napkin (Step 1). But when they try to hand the blueprint to a strict construction foreman (the computer) to build it, they fail miserably.

• The Result: On the hard problems (FATE-H and FATE-X), the robots' "napkin drawings" (English reasoning) were actually quite good. They understood the math!
• The Failure: But when they tried to turn those drawings into the strict "construction code" (Lean), they failed. They hallucinated tools that didn't exist, used the wrong grammar, or forgot to close a parenthesis.

The Bottom Line: The robots aren't bad at math; they are bad at speaking the language of the computer perfectly. It's like having a brilliant poet who can't type without making typos.

The "Specialist" vs. The "Generalist"

The paper also compared two types of robots:

• The Generalist: A smart robot trained on everything (like a well-read human).
• The Specialist: A robot trained only on math proofs.

The Surprise: The Generalist actually did better at the "napkin drawing" stage. Why? Because the Specialist robot had been trained so hard to follow strict rules that it lost its ability to "think outside the box" or admit when it was wrong. It got stuck in a loop of trying to force a square peg into a round hole, whereas the Generalist was better at realizing, "Wait, this approach isn't working, let me try a different angle."

What Does This Mean for the Future?

The paper suggests that to get AI to do real, cutting-edge math research, we can't just train them to be better "coders." We need to:

1. Separate the tasks: Have one AI be the "Idea Person" (writing the English proof) and a different AI be the "Translator" (turning it into code).
2. Teach them to reflect: We need to teach these robots how to look at their own mistakes, say "I was wrong," and try a completely new path, rather than just stubbornly trying to fix the code.

In short: We have built robots that are great at solving puzzles, but they are still terrible at writing the rigorous, error-free manuals required to build the future of mathematics. The FATE benchmark is the ruler we need to measure how far we still have to go.

Technical Summary

Here is a detailed technical summary of the paper "FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels".

1. Problem Statement

Current Large Language Models (LLMs) have demonstrated impressive capabilities in formal theorem proving on contest-based benchmarks (e.g., IMO, Putnam) and introductory university-level mathematics. However, these benchmarks fail to reflect the depth, breadth, and abstraction of modern mathematical research.

• The Gap: Contest problems often rely on clever tricks rather than systematic theoretical frameworks, while introductory courses lack the high level of abstraction found in research.
• The Bottleneck: As mathematical proofs become more advanced, human verification becomes slow and unscalable. Formal verification (e.g., via Lean) is the solution, but current models struggle to bridge the gap between natural language reasoning and rigorous formal code, particularly in advanced fields like abstract and commutative algebra.
• The Need: There is a lack of benchmarks that span from undergraduate exercises to PhD qualifying exam levels and beyond, specifically designed to test the ability of AI to handle research-level formalization.

2. Methodology: The FATE Benchmark Series

The authors introduce FATE (Formal Algebra Theorem Evaluation), a progressive series of benchmarks focused on abstract and commutative algebra. The series consists of three tiers of increasing difficulty:

1. FATE-M (Modified/Expanded): Extends the existing undergraduate-level benchmark (from 141 to 150 problems) with improved formalization details.
2. FATE-H (Hard): 100 new problems at the level of honors course exams or graduate-level coursework.
3. FATE-X (Expert): 100 new problems at the level of PhD qualifying exams or beyond.

Key Characteristics of FATE-X:

• It is the first formal benchmark to exceed PhD qualifying exam difficulty.
• Its content surpasses the current coverage of Mathlib (the standard Lean mathematical library). Approximately 38% of FATE-X problems require new definitions (e.g., local complete intersections, Gorenstein rings) that do not exist in Mathlib, forcing models to derive necessary lemmas or formulate new definitions.

Curation Process:

• Data Sources: Problems were selected from standard textbooks (e.g., Lang, Eisenbud), PhD qualifying exams, and research papers (e.g., Stacks Project).
• Workflow: A rigorous three-stage process involving:
  1. Collection: 400 candidate problems curated by ~20 postdocs/PhDs in pure algebra.
  2. Formalization: 200 problems formalized in Lean by 5 Mathlib contributors (including those working on the formalization of Fermat's Last Theorem).
  3. Review: Double-blind review by experts with strong Lean backgrounds, followed by external verification.

3. Experimental Setup

The authors evaluated state-of-the-art models using a two-stage generation pattern observed in model outputs:

1. Natural Language Reasoning: Generating a Chain-of-Thought (CoT) proof.
2. Formalization: Translating the CoT into Lean 4 code.

Models Evaluated:

• General Reasoning Models: o3, Gemini-2.5-Pro, Claude-4-Sonnet-thinking, DeepSeek-R1, Qwen3.
• Specialized Theorem Provers: DeepSeek-Prover-V2-671B, Goedel-Prover-V2-32B, Kimina-Prover-72B.

Metrics:

• Formal Accuracy: pass@64 (success if at least one of 64 attempts compiles and verifies in Lean).
• Natural Language Accuracy: Manual evaluation by human experts on the correctness of the intermediate natural language proofs (pass@1).

4. Key Results

A. Performance Collapse on Frontier Problems

There is a stark performance drop as difficulty increases:

• FATE-M: Models achieve reasonable success (e.g., DeepSeek-Prover-V2 at 62.7%, o3 at 51.3%).
• FATE-H: Performance drops drastically. The best model (DeepSeek-Prover-V2) achieves only 3.0% accuracy.
• FATE-X: 0% accuracy for all models. No model produced a single valid Lean proof for the most difficult problems.

B. The Formalization Bottleneck

A critical finding is the decoupling between natural language reasoning and formalization:

• Natural Language vs. Formal: On FATE-H, DeepSeek-R1 achieved 71.0% accuracy in natural language reasoning but 0.0% in formalization.
• Conclusion: The primary bottleneck is not the mathematical reasoning itself, but the translation of correct informal reasoning into precise formal code. Models understand the math but fail to implement it in Lean.

C. Error Analysis

The authors classified formalization errors into four categories:

1. Mathlib Hallucinations: Generating non-existent theorems or incorrect definitions (Most common).
2. Lean Proficiency Issues: Syntax errors, type system misunderstandings, and incorrect tactic usage (Most common).
3. General Capability Issues: Repetitive loops, leaving sorry placeholders, or header mismatches.
4. Misalignment: The formal proof diverges from the natural language reasoning (Least common).

D. General vs. Specialized Models

• General Reasoning (DeepSeek-R1): Outperformed specialized provers in natural language reasoning (71% vs. 39% for DeepSeek-Prover-V2 on FATE-H).
• Effective Reflection: General models demonstrated a superior ability to "reflect"—locating, diagnosing, and repairing logical flaws in their reasoning. Specialized provers often engaged in "formal reflection" (changing direction without logical repair) or "cheating" (using sorry to bypass logic), leading to lower natural language accuracy.

5. Key Contributions

1. Progressive Benchmark Creation: Introduced FATE-H and FATE-X, creating the first benchmark series spanning from undergraduate to post-PhD research levels in algebra. FATE-X is unique in requiring definitions beyond current Mathlib.
2. Baseline Establishment: Established that the state-of-the-art for formal proving on research-level math is currently near zero (0% on FATE-X, 3% on FATE-H).
3. Two-Stage Analysis: Demonstrated that the failure in formal proving is primarily due to the formalization stage, not the reasoning stage, revealing a functional decoupling in current models.
4. Insight on Specialization: Found that specialized theorem provers may suffer from reduced "effective reflection" capabilities compared to general-purpose reasoning models, hindering their performance even at the reasoning stage.

6. Significance and Future Directions

• Research Roadmap: FATE provides essential checkpoints for measuring progress toward AI-assisted mathematical research.
• Decoupled Approach: The findings suggest that a decoupled architecture (separate models for natural language reasoning and formalization) might be more effective than end-to-end generation, as the skills required for each stage are distinct.
• Training Methodology: Future work must address how to train models to simultaneously possess precise formalization skills and robust meta-reasoning (reflection) capabilities. The current trend of specialized reinforcement learning for formalization appears to have degraded the model's general reasoning and reflection abilities.

In summary, FATE reveals that while LLMs are approaching saturation on contest math, they are currently incapable of handling research-level formal mathematics, primarily due to a failure in translating abstract reasoning into rigorous code, rather than a lack of mathematical insight.