HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification

• URL: http://arxiv.org/abs/2603.15617v1
• Date: Mon, 16 Mar 2026 17:59:53 GMT
• Title: HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification
• Abstract summary: We introduce HorizonMath, a benchmark of over 100 predominantly unsolved problems spanning 8 domains in computational and applied mathematics.<n>Our benchmark targets a class of problems where discovery is hard, requiring meaningful mathematical insight, but verification is computationally efficient and simple.
• Score: 54.06301039725887
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Can AI make progress on important, unsolved mathematical problems? Large language models are now capable of sophisticated mathematical and scientific reasoning, but whether they can perform novel research is still widely debated and underexplored. We introduce HorizonMath, a benchmark of over 100 predominantly unsolved problems spanning 8 domains in computational and applied mathematics, paired with an open-source evaluation framework for automated verification. Our benchmark targets a class of problems where discovery is hard, requiring meaningful mathematical insight, but verification is computationally efficient and simple. Because these solutions are unknown, HorizonMath is immune to data contamination, and most state-of-the-art models score near 0%. Existing research-level benchmarks instead rely on formal proof verification or manual review, both of which are expensive to scale. Using this platform, we find two problems for which GPT 5.4 Pro proposes solutions that improve on the best-known published results, representing potential novel contributions (pending expert review). We release HorizonMath as an open challenge and a growing community resource, where correct solutions to problems in the unsolved problem classes could constitute novel results in the mathematical literature.

Related papers

• 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)
• MIRA-Math: A Benchmark for Minimal Information Requesting and Mathematical Reasoning [0.0]
  MIRA-Math is a benchmark for solving problems whose full latent state has a unique answer, but whose solver-facing view is missing exactly one necessary atomic fact.<n>The solver must request the missing information in natural language under a strict budget and then integrate the returned fact into an exact final answer.<n> MIRA-Math contains 2,310 generated instances from 22 typed mathematical families spanning algebra, probability, linear systems, discrete structures, signal processing, Markov chains, circuits, computation, and numerical boundary-value problems.
  arXiv  Detail & Related papers  (2026-07-08T13:23:56Z)
• RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics [30.778394290919582]
  Existing benchmarks for evaluating mathematical reasoning in large language models (LLMs) rely primarily on competition problems, formal proofs, or artificially challenging questions.<n>We introduce RealMath, a novel benchmark derived directly from research papers and mathematical forums that assesses LLMs' abilities on authentic mathematical tasks.
  arXiv  Detail & Related papers  (2025-05-18T23:32:46Z)
• 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)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  We advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level.<n>We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.
  arXiv  Detail & Related papers  (2024-12-20T17:19:24Z)
• UTMath: Math Evaluation with Unit Test via Reasoning-to-Coding Thoughts [7.856746367263317]
  This paper introduces the UTMath Benchmark, a robust evaluation framework designed to assess Large Language Models.<n>It comprises 1,053 cutting-edge problems spanning nine mathematical domains, with an average of 68 test cases per problem.<n>The best-performing model, o1-mini, solving only 32.57% of the problems, followed by o1-preview at 27.16%, and GPT-4o at 26.93%.
  arXiv  Detail & Related papers  (2024-11-11T18:59:02Z)
• FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI [8.32177898148028]
  FrontierMath is a benchmark of hundreds of original, exceptionally challenging mathematics problems crafted and vetted by expert mathematicians.<n>Current state-of-the-art AI models solve under 2% of problems, revealing a vast gap between AI capabilities and the prowess of the mathematical community.<n>As AI systems advance toward expert-level mathematical abilities, FrontierMath offers a rigorous testbed that quantifies their progress.
  arXiv  Detail & Related papers  (2024-11-07T17:07:35Z)
• MathScale: Scaling Instruction Tuning for Mathematical Reasoning [70.89605383298331]
  Large language models (LLMs) have demonstrated remarkable capabilities in problem-solving. However, their proficiency in solving mathematical problems remains inadequate. We propose MathScale, a simple and scalable method to create high-quality mathematical reasoning data.
  arXiv  Detail & Related papers  (2024-03-05T11:42:59Z)
• MathCoder: Seamless Code Integration in LLMs for Enhanced Mathematical Reasoning [52.97768001837269]
  We present a method to fine-tune open-source language models, enabling them to use code for modeling and deriving math equations. We propose a method of generating novel and high-quality datasets with math problems and their code-based solutions. This approach yields the MathCoder models, a family of models capable of generating code-based solutions for solving challenging math problems.
  arXiv  Detail & Related papers  (2023-10-05T17:52:09Z)
• Measuring Mathematical Problem Solving With the MATH Dataset [55.4376028963537]
  We introduce MATH, a dataset of 12,500 challenging competition mathematics problems. Each problem has a full step-by-step solution which can be used to teach models to generate answer derivations and explanations. We also contribute a large auxiliary pretraining dataset which helps teach models the fundamentals of mathematics.
  arXiv  Detail & Related papers  (2021-03-05T18:59:39Z)

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.