Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification

Erik Y. Wang, Sumeet Motwani, James V. Roggeveen, Eliot Hodges, Dulhan Jayalath, Charles London, Kalyan Ramakrishnan, Flaviu Cipcigan, Philip Torr, Alessandro Abate

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.

HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification

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.
Paper Structure (23 sections, 13 equations, 4 figures, 1 table)

This paper contains 23 sections, 13 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. AI-Driven Mathematical Discovery
  3. Mathematical Reasoning Benchmarks
  4. Recent Progress
  5. Research-Level Benchmarks
  6. Related Domains and Datasets
  7. Benchmark Design and Evaluation
  8. Design Principles
  9. Curation Procedure
  10. Dataset Composition
  11. Output types:
  12. Solvability levels:
  13. Mathematical domains:
  14. Admissible Solutions for Closed Forms
  15. Automated Evaluation
  16. ...and 8 more sections

Figures (4)

  • Figure 1: Problem inclusion pipeline for HorizonMath. Candidate problems pass through two stages: automatable evaluation (solutions must be concrete and machine-verifiable) and meaningful discovery (solving requires genuine insight and advances the research frontier). Dashed arrows indicate problem rejection.
  • Figure 2: Benchmark composition by solvability level (left) and mathematical domain (right). The benchmark comprises 101 problems in total, distributed across several areas of mathematics and physics.
  • Figure 3: Automated evaluation pipeline. A model generates a proposed solution, which is screened by a compliance checker that rejects forbidden operations. Admissible solutions are routed to one of three evaluation modes: numeric comparison against a ground-truth value, benchmark scoring for improvement over the best-known result, and construction checking to validate all required structural properties.
  • Figure 4: Model performance on the benchmark for Claude Opus 4.6, Gemini 3.1 Pro, and GPT 5.4 Pro. Accuracy on the full dataset is shown on the left, where the dotted line (the human baseline) indicates the ten problems solved by humans. In the 7% figure for GPT 5.4 Pro, five problems are from the solvability 0 tier, and two are from the solvability 1 tier. Model performance on the set of solvability 0 problems is shown in the center. The number of solutions beating existing human optimizations is shown on the right, in which GPT 5.4 Pro is the only model of the three to produce novel solutions.