IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

• URL: http://arxiv.org/abs/2512.00997v1
• Date: Sun, 30 Nov 2025 17:40:13 GMT
• Title: IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch
• Abstract summary: We introduce IndiMathBench, a human-verified benchmark designed to evaluate mathematical theorem proving.<n>IndiMathBench is composed of 312 formal Lean 4 theorems paired with their corresponding informal problem statements, sourced from Indian Mathematics Olympiads.
• Score: 8.80477323574638
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce IndiMathBench, a human-verified benchmark designed to evaluate mathematical theorem proving, curated using an AI-powered human-assisted pipeline for formalizing natural language problems in Lean. IndiMathBench is composed of 312 formal Lean 4 theorems paired with their corresponding informal problem statements, sourced from Indian Mathematics Olympiads. Through category-based retrieval, iterative compiler feedback, and multi-model ensembles, our pipeline generates candidate formalizations that experts efficiently validate via an interactive dashboard with automated quality summaries. Evaluation across multiple frontier models demonstrates that autoformalization remains challenging, with substantial gaps between syntactic validity and semantic correctness, while theorem proving success rates remain low even with iterative refinement, demonstrating that \benchmark~presents a challenging testbed for mathematical reasoning. IndiMathBench is available at https://github.com/prmbiy/IndiMathBench.

Related papers

• MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize [38.37332307303914]
  MathAdv is a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics.<n>We show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures.
  arXiv  Detail & Related papers  (2026-08-26T07:12:54Z)
• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents.<n>We provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis.
  arXiv  Detail & Related papers  (2026-07-08T17:46:36Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• Automated Conjecture Resolution with Formal Verification [21.763678203045973]
  We propose an automated framework for tackling research-level mathematical problems.<n>Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon.<n>Using this framework, we automatically resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement.
  arXiv  Detail & Related papers  (2026-04-04T16:35:16Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• EternalMath: A Living Benchmark of Frontier Mathematics that Evolves with Human Discovery [23.517907682810932]
  We propose a fully automated, theorem-grounded pipeline for evaluating frontier mathematical reasoning.<n>The pipeline transforms recent peer-reviewed mathematical literature into executable and verifiable reasoning tasks.<n>Applying this pipeline yields textbfEternalMath, an evolving evaluation suite derived from contemporary research papers.
  arXiv  Detail & Related papers  (2026-01-04T06:40:25Z)
• Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
  We propose leveraging theoretical computer science (TCS) as a scalable source of rigorous proof problems.<n>We demonstrate this approach on two TCS domains: Busy Beaver problems, which involve proving bounds on Turing machine halting behavior, and Mixed Boolean Arithmetic problems, which combine logical and arithmetic reasoning.<n>Our framework automatically synthesizes problems with parallel formal (Lean4) and informal (Markdown) specifications, creating a scalable pipeline for generating verified proof challenges.
  arXiv  Detail & Related papers  (2025-08-21T14:15:40Z)
• Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems [9.041749463376599]
  We propose Proof2Hybrid, a framework that synthesizes high-quality, proof-centric benchmarks from natural language mathematical corpora.<n>Our framework and benchmark pave the way for a new wave of in-depth research into the mathematical intelligence of AI systems.
  arXiv  Detail & Related papers  (2025-08-04T08:59:36Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  We present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems.<n>We introduce a novel human-in-the-loop autoformalization pipeline that integrates statement autoformalization, semantic verification, and negation-based disproof filtering strategies.<n>Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations.
  arXiv  Detail & Related papers  (2025-05-05T15:37:00Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATH is a novel Olympiad-level mathematical benchmark designed to rigorously test the complex reasoning capabilities of LLMs.<n>OlymMATH features 200 meticulously curated problems, each manually verified and available in parallel English and Chinese versions.
  arXiv  Detail & Related papers  (2025-03-27T11:20:17Z)
• PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
  We introduce PromptCoT, a novel approach for automatically generating high-quality Olympiad-level math problems.<n>The proposed method synthesizes complex problems based on mathematical concepts and the rationale behind problem construction.<n>Our method is evaluated on standard benchmarks including GSM8K, MATH-500, and AIME2024, where it consistently outperforms existing problem generation methods.
  arXiv  Detail & Related papers  (2025-03-04T06:32:30Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation.<n>For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it.<n>As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  This paper explores the use of Large Language Models (LLMs) to generate formal proof steps and complete formalized proofs. The goal is to determine how AI can be leveraged to assist the mathematical formalization process and improve its performance.
  arXiv  Detail & Related papers  (2024-09-09T18:21:28Z)
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics [7.607254619341369]
  We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3. We report baseline results on statement autoformalization via in-context learning.
  arXiv  Detail & Related papers  (2023-02-24T03:28:46Z)
• Formal Mathematics Statement Curriculum Learning [64.45821687940946]
  We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems.
  arXiv  Detail & Related papers  (2022-02-03T00:17:00Z)
• NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
  We develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs. NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources. We benchmark strong neural methods on mathematical reference retrieval and generation tasks.
  arXiv  Detail & Related papers  (2021-03-24T03:14:48Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.