IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

This paper introduces IndiMathBench, a human-verified benchmark of 312 formal Lean 4 theorems derived from Indian Mathematics Olympiads, which utilizes an AI-powered human-assisted pipeline to address the scarcity of high-quality training data and reveals significant challenges in current autoformalization and theorem proving capabilities.

The Gist

Imagine you are trying to teach a brilliant but slightly literal-minded robot how to speak "Math."

The robot is very good at reading English math problems (like "Prove that this triangle is isosceles") and can write code that looks like a math proof. But here's the catch: the robot often writes code that compiles (runs without crashing) but is actually nonsense logically. It's like a student who writes a perfect essay with beautiful grammar but completely misses the point of the question.

This paper, INDIMATHBENCH, is about building a better "exam" to test these robots and a new "study group" to help them learn.

Here is the breakdown in simple terms:

1. The Problem: The "Data Famine"

For a long time, researchers have wanted to test AI on hard math problems. But they ran out of good test questions.

• The Old Tests: Existing tests (like MiniF2F) are like a small library with only 1,000 books. Many of them are old, and the AI might have already "cheated" by memorizing the answers during its training.
• The Human Bottleneck: To make a new, fair test, you need a human expert to translate every single math problem into a strict computer language called Lean. This is like translating a novel into a secret code where every comma matters. It takes forever and is incredibly expensive.

2. The Solution: The "Human-AI Study Group"

The authors created INDIMATHBENCH, a new library of 312 hard math problems from Indian Math Olympiads (which are famous for being tricky and creative).

But they didn't just hire 312 humans to do the work. They built a pipeline (a workflow) that acts like a super-efficient study group:

• The AI Students: They used 12 different top-tier AI models to try translating the problems into Lean code.
• The "Textbook" (Retrieval): Before the AI guesses, the system gives it a "cheat sheet" of relevant math rules from the Lean library so it doesn't make up fake rules.
• The "Tutor" (Compiler Feedback): If the AI writes code that has a syntax error (like a typo), the computer compiler yells, "This doesn't work!" The AI then tries again, fixing the error. It does this up to 6 times per problem.
• The "Group Study" (Ensemble): They ask 12 different AIs to solve the same problem. If one AI gets the logic right but the syntax wrong, and another gets the syntax right but the logic wrong, the system can spot the difference.
• The Human Teacher: Finally, a human expert looks at the AI's best attempts. They don't start from scratch; they just fix the small mistakes the AI missed.

The Result: This "Human-AI" method was 3.5 times faster than a human doing it alone, but it still ensured every single answer was 100% correct.

3. The Big Discovery: "Syntax vs. Semantics"

The authors tested the world's smartest AI models on this new benchmark. The results were a bit of a reality check:

• The "Good at Grammar" Problem: The AIs are getting really good at writing code that looks correct to the computer (it compiles). It's like a student who writes a perfect sentence structure but uses the wrong words.
• The "Meaning" Gap: When you check if the math logic is actually true (does the proof actually work?), the AIs fail miserably.
  • The Stat: Even with 10 tries and a lot of help, the best AI (GPT-5) only solved about 11% of the problems correctly.
  • The Geometry Struggle: The AIs were especially bad at geometry. It's like they can do algebra well but get completely lost when asked to visualize shapes and angles.

4. Why This Matters

Think of this paper as a new, harder driving test for AI.

• Before, the tests were easy, and the cars (AIs) looked like they were driving perfectly.
• Now, with INDIMATHBENCH, we see that while the cars can turn the steering wheel (write code), they often don't know how to steer around a real obstacle (solve the actual math logic).

The Takeaway:
We can't just rely on AI to do math for us yet. But, by using AI to do the heavy lifting (drafting the code) and humans to do the final quality check (fixing the logic), we can build massive libraries of math problems much faster. This helps us train better AIs for the future, even if today's AIs still need a human to hold their hand.

In short: The paper says, "AI is getting better at the form of math, but it still needs a human to teach it the substance."

Technical Summary

1. Problem Statement

The paper addresses the critical bottleneck in the development of Automated Theorem Provers (ATPs) and Large Language Models (LLMs) for mathematical reasoning: the scarcity of high-quality, human-verified formal training data.

• Data Scarcity & Contamination: Existing benchmarks (e.g., MINIF2F, PutnamBench) are small (approx. 1,000 problems), narrow in scope (often missing geometry and combinatorics), and increasingly contaminated by pretraining data, obscuring genuine reasoning capabilities.
• Annotation Bottleneck: Creating new benchmarks requires experts to manually formalize problems in Lean, a process that is time-consuming, resource-intensive, and difficult to scale.
• Semantic Gap: While LLMs have improved at generating syntactically valid code, they struggle with semantic correctness (ensuring the formal statement matches the mathematical intent), particularly in complex domains like geometry.

2. Methodology: The Human-AI Collaborative Pipeline

The authors introduce INDIMATHBENCH, a benchmark of 312 problems from Indian Mathematical Olympiads (RMO and INMO), created via a scalable, human-AI collaborative pipeline.

A. Dataset Composition

• Source: 312 problems from Indian Regional and National Mathematical Olympiads.
• Domains: Geometry (98), Algebra (92), Number Theory (77), and Set Theory/Combinatorics (45).
• Characteristics: Unlike Western benchmarks, these problems strictly adhere to high-school curricula (excluding calculus) but feature high internal diversity, requiring multi-step reasoning, auxiliary constructions, and non-standard techniques.

B. The Autoformalization Pipeline (Algorithm 1)

The pipeline transforms natural language problems into Lean 4 theorems through three iterative steps:

1. Category-Based Retrieval:
   • Problems are classified into domains.
   • An agent (Claude Sonnet 4) with bash access to the Mathlib repository extracts relevant definitions, theorems, and syntax patterns specific to that category.
   • This creates a static context (documentation) for each domain to prevent hallucinations and guide the LLM.
2. Iterative Refinement with Compiler Feedback:
   • LLMs generate formal statements conditioned on the retrieved context.
   • Outputs are compiled in Lean 4. Errors are parsed and fed back to the model.
   • This loop runs up to 6 times, achieving syntactic validity for 95.3% of problems.
3. Multi-Model Ensemble & Comparative Analysis:
   • 12 frontier models (e.g., GPT-5, Claude Opus 4, Gemini 2.5 Pro) generate candidates for each problem.
   • An LLM summarizes these candidates, highlighting shared errors, missing conditions, and the most promising fragments.
   • This allows human experts to merge partial correct outputs (e.g., taking a correct condition from Model A and a correct structure from Model B).

C. Human-AI Dashboard

A custom VS Code Extension was developed to facilitate expert review. It integrates:

• Real-time Lean compilation and error tracing.
• Aggregated LLM summaries to reduce cognitive load.
• Tools to merge candidates and edit annotations efficiently.
• Human Guarantee: Every theorem in the final benchmark is manually verified by two experts for both correctness and stylistic quality.

3. Key Contributions

1. INDIMATHBENCH: A new, human-verified benchmark of 312 Lean 4 theorems covering diverse Olympiad-level problems, specifically addressing the underrepresentation of geometry and combinatorics in existing datasets.
2. Scalable Formalization Pipeline: A novel workflow combining category-based retrieval, iterative compiler feedback, and multi-model ensembles that significantly accelerates human annotation.
3. VS Code Annotation Tool: An open-source extension enabling efficient human-AI collaboration for formalizing mathematical statements.
4. Controlled Efficiency Study: A study demonstrating that the proposed system reduces annotation time by 3.5x compared to manual formalization and 2.2x compared to using masked LLM candidates without summaries.

4. Experimental Results

A. Autoformalization Performance (Generation)

• Metrics: Evaluated using Bidirectional Equivalence (BEq) (semantic equivalence) and Generalized Tree Edit Distance (GTED) (syntactic similarity).
• Top Performers: Claude Opus 4 achieved the best results (67/312 BEq passes, 0.51 mean GTED), followed by GodelProverV2 and GPT-5.
• Semantic vs. Syntactic Gap: While compilation success rates were high (e.g., 77.9% for Claude Opus 4), semantic correctness (BEq) remained low (21.5%). This highlights that models can generate valid Lean code that is mathematically incorrect.
• Geometry Difficulty: Geometry problems were the most challenging; among the top 3 models, only 12 out of 108 BEq-passing problems were geometry-based, indicating a specific weakness in spatial reasoning and coordinate-free formalization.

B. Automated Theorem Proving (ATP) Performance

• Single-Turn: Extremely low success rates. Only 1 problem (out of 312) was solved by any model in a single turn (relying on existing Mathlib lemmas like the Pitot theorem).
• Multi-Turn (10 turns with feedback):
  • GPT-5 achieved the highest success rate: 36/312 (11.5%) on INDIMATHBENCH.
  • Performance on PutnamBench was comparable (28/660, ~4%), suggesting INDIMATHBENCH is a similarly difficult, uncontaminated testbed.
  • No geometry problems were solved by any model in the multi-turn setting.

C. Efficiency Study

• Manual Formalization: ~14 minutes/problem.
• Masked Candidates (LLMs only): ~9 minutes/problem (1.6x speedup).
• Full System (LLMs + Summaries + Dashboard): ~4 minutes/problem (3.5x speedup).
• Insight: The LLM-generated summaries were crucial, allowing experts to identify errors in top-ranked candidates and merge correct fragments from other generations.

5. Significance and Conclusion

• Benchmarking Reality: INDIMATHBENCH reveals a substantial gap between current LLM capabilities and the rigor required for formal mathematics. Even frontier models struggle to prove more than 11% of problems, even with iterative refinement.
• Human-in-the-Loop Necessity: The paper demonstrates that fully automated formalization is currently insufficient. The most effective approach is a hybrid pipeline where AI handles syntax generation and error correction, while humans provide semantic oversight and logical verification.
• Community Impact: By releasing the dataset and the VS Code tool, the authors provide the community with a fresh, uncontaminated benchmark and a scalable workflow to expand formal mathematics corpora, which is essential for training future, more capable theorem provers.

In summary, INDIMATHBENCH establishes a new standard for evaluating mathematical reasoning in AI, proving that while LLMs are improving at syntax, they still lack the deep semantic understanding required for complex theorem proving, necessitating continued human-AI collaboration.