Source-linked AI summary
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
TL;DR
AI progress toward mathematical discovery is difficult to measure because existing benchmarks mostly use known solutions, while genuinely unsolved problems are hard to verify. HorizonMath addresses this gap with over 100 predominantly unsolved problems and automated verification based on numerical comparison and deterministic checkers. Most frontier models score near 0%, while GPT 5.4 Pro proposes potentially novel improvements on two published optimization problems, pending expert review.
Problem
Existing mathematics benchmarks mostly evaluate known solutions, leaving limited evidence about whether AI systems can produce novel mathematical results.
Method
HorizonMath combines over 100 predominantly unsolved problems with open-source verification scripts using high-precision numerical comparison and deterministic constraint-checkers.
Results
Current frontier models score near 0%, while GPT 5.4 Pro proposes potentially novel improvements on two solvability-1 optimization problems.
Takeaways & Limitations
HorizonMath provides a concrete, reproducible signal of progress toward autonomous mathematical research and an open challenge for community contributions.
Takeaways & Limitations
Matching a high-precision numerical reference does not formally prove a closed-form expression, and the compliance checker may accept loopholes or reject valid constructions.
Abstract
from arXiv · showhide
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.
1 Introduction
HorizonMath addresses the lack of scalable benchmarks for AI-driven mathematical discovery by pairing predominantly unsolved problems with automated verification. Its design targets problems that are difficult to solve but efficient to check, while supporting contamination-resistant and standardized evaluation.
- Motivation: Existing mathematics benchmarks mostly test problem-solving on known answers, offering minimal evidence about whether AI can produce novel mathematical results.Saturated datasets include MATH and GSM8K, while harder Olympiad and graduate-level benchmarks still use problems with known solutions.
- Design rationale: The benchmark targets a generator-verifier gap: candidate solutions require substantial insight but can be checked efficiently by deterministic computation.The identified classes include closed-form discovery, optimization beyond a current baseline, and existence or construction problems.
- Benchmark contribution: HorizonMath contains over 100 predominantly unsolved problems across 8 domains, with unknown solutions that are absent from training corpora.A correct model-generated solution could therefore signal genuine reasoning ability and autonomous discovery.
- Verification: Automated verification replaces much of the traditional human-review bottleneck with high-precision numerical comparison and deterministic constraint checking.The framework provides a fast, objective correctness signal while filtering inadmissible solutions.
- Infrastructure: The framework is open-source and standardized, releasing problem definitions, ground-truth computations, and verifier scripts for reproducible evaluation.The authors describe HorizonMath as an ongoing community effort and open challenge.
2 AI-Driven Mathematical Discovery
Recent AI systems have produced new mathematical results through program search, autonomous reasoning, and human-AI collaboration, motivating benchmarks for genuinely unsolved problems. Existing research-level evaluations improve difficulty but often remain private, manually graded, or limited in scale.
- Existing benchmarks: Frontier benchmarks such as GSM8K and MATH are approaching saturation, while Olympiad and graduate-level datasets still evaluate problems with known solutions.These benchmarks therefore do not directly assess novel mathematical discovery.
- AI discovery systems: FunSearch and AlphaEvolve improved published bounds or heuristics through program evolution across combinatorics, geometry, number theory, and related domains.Their results demonstrate progress on open-ended construction and optimization tasks.
- Human-AI collaboration: Human-AI collaborations have resolved open problems across theoretical computer science, information theory, physics, and mathematics, sometimes producing constructions later proved correct.The cited examples include analytic expressions and a closed-form Hamiltonian-cycle construction.
- Toward autonomy: Recent autonomous systems have produced new mathematical results, including papers with minimal human intervention and an Erdős problem resolved with a Lean proof.These developments further increase demand for systematic discovery evaluations.
- Evaluation gap: FrontierMath, IMProofBench, and First Proof provide research-level problems but rely partly on private infrastructure, expert grading, small scale, or proof-oriented tasks.FrontierCS offers automated scoring for open-ended optimization, but it is focused on computer science rather than mathematics.
3 Benchmark Design and Evaluation
HorizonMath selects concrete mathematical outputs that are difficult to discover yet objectively verifiable, then organizes them by output type, solvability, and domain. Its automated pipeline screens proposed code and routes admissible solutions to numerical, benchmark, or construction checks.
- Design principles: Each problem requires an explicit mathematical object and a simple deterministic verification procedure rather than a natural-language proof.Eligible tasks must also demand long-horizon reasoning and meaningful discovery.
- Dataset composition: The preliminary benchmark contains 101 problems classified by structural output type, solvability level, and mathematical domain.Figure 2 presents the composition by solvability and domain.
- Output types: Constant discovery is the largest output category, followed by constructions that improve discrete mathematical objects over existing baselines.Other tasks generate computable functions with specified properties or discover general formulas.
- Solvability levels: Solvability levels range from Level 0 calibration problems with known closed forms to Level 3 problems that may be conjectured unsolvable or lack finite closed forms.Levels 1 and 2 represent increasing demands for known techniques, near-term capabilities, or major methodological breakthroughs.
- Mathematical domains: The benchmark spans eight mathematical subdomains, with analysis and mathematical physics as the largest categories.Geometry and number theory emphasize packing, extremal configurations, and explicit sequence values, while combinatorics and coding theory emphasize discrete constructions.
- Admissible solutions: Closed-form candidates must use permitted symbolic operations and exclude unevaluated integrals, infinite series, limits, implicit definitions, and numerical approximations presented as exact values.The prompt reveals at most five significant figures to discourage symbolic parameter fitting to the reference value.
- Automated evaluation: The evaluation pipeline uses a compliance checker before routing admissible solutions to numeric comparison, benchmark scoring, or construction checking.These modes respectively test agreement with a reference, improvement over a best-known result, or satisfaction of required structural properties.
4 Automated Evaluation
HorizonMath uses a fully automated, reproducible pipeline that evaluates several problem types with numerical comparison or deterministic validators. Numerical matches provide robust evidence but remain conjectural without formal proof.
- The pipeline generates self-contained Python solutions and applies admissibility checks before evaluation.Models return symbolic expressions or JSON-serializable constructions under restricted operations.
- Ground-truth problems accept expressions matching high-precision references to min(20, D) verified decimal digits.References are typically computed through integration or series expansion.
- Benchmark-best-known problems pass only when problem-specific validators confirm a strict improvement over the published baseline.Solutions are additionally ranked by relative improvement on the relevant metric.
- Construction problems use deterministic, exhaustive pass/fail validators to check all required object properties without baseline comparison.
- High-precision numerical agreement does not formally prove a closed form, so such solutions remain conjectures until proven.Constructions beating published bounds are instead verified deterministically by checking their required properties.
5 Representative Problem Examples
The representative examples span symbolic discovery problems in special functions, including an unknown fifth Airy-function moment and general spheroidal eigenvalue formulas. Models must submit accurate, restricted mpmath implementations, even when the result is unproven.
- Both representative ground-truth problems require models to discover symbolic closed forms evaluated through restricted mpmath functions.The prompt specifies Python functions and limits permitted operations to mpmath-supported constants and functions.
- Fifth Moment of the Airy Function: The fifth Airy-function moment a5 lacks a known symbolic expression despite a numerical value near 0.0013493.The task asks for a symbolic closed form for this fifth moment.
- Fifth Moment of the Airy Function: The Airy-moment task accepts an accurate candidate, including a conjecture, provided it satisfies the stated requirements.The required output is an mpmath Python function computing the proposed expression.
- Angular Prolate Spheroidal Eigenvalues: The spheroidal-eigenvalue example asks for a symbolic λ_n(c) valid for integer n ≥0 and real c ≥0.The problem concerns a Sturm–Liouville eigenvalue function whose general symbolic closed form remains undiscovered.
3. Minimum-Scope Difference Triangle Set (7,5)
The (7,5)-difference triangle set example is a combinatorial optimization problem: construct a valid array with distinct within-row differences while minimizing its maximum entry below the current bound.
- Problem definition: A (n, k)-DTS is an n × (k + 1) array with strictly increasing, normalized rows.
- Problem definition: Validity requires every positive within-row difference to be distinct across all rows.The difference set is defined over every pair of positions within each row.
- Optimization objective: The scope objective is m(A) = max_i,j a_i,j, so lower maximum entries are preferred.
- Optimization objective: The task seeks a valid (7, 5)-DTS with scope strictly below the current best-known upper bound of 113.The cited 2026 source improved the previous best of 113.
- Output format: The example requires the construction to be returned as a Python dictionary.
6 Evaluation Results
GPT 5.4 Pro was the only evaluated model to make progress on solvability-tier 1–3 problems, proposing two potentially novel optimization improvements. It also solved more calibration problems, although some evaluations were unavailable because of API errors.
- GPT 5.4 Pro was the only model making progress on solvability tier 1–3 problems.It proposed potentially novel solutions for Thin-Triangle Kakeya and diagonal Ramsey-number optimization problems.
- The two proposed solutions require expert inspection before being treated as novel results.Gemini 3.1 Pro and Claude Opus 4.6 produced no novel solutions passing the compliance checker or verifiers.
- Diagonal Ramsey Numbers: The Ramsey-number construction achieved c ≈3.6961, below the baseline of roughly 3.7992.The authors validated it with interval arithmetic on [0.001, 1] and an analytic construction over (0, 0.001].
- Thin-Triangle Kakeya: GPT 5.4 Pro reduced the Thin-Triangle Kakeya validator area by around 8.44% relative to the Keich baseline.Exact rational arithmetic verification provided high confidence in the construction’s correctness.
- Calibration: On 10 solvability-0 calibration problems, GPT 5.4 Pro solved 5, while Gemini 3.1 Pro and Claude Opus 4.6 each solved 3.API errors prevented results for 13 problems, including one calibration problem, for GPT 5.4 Pro.
7 Discussion
HorizonMath combines predominantly unsolved problems with automated verification to measure progress toward mathematical discovery. Its current results show near-zero frontier-model performance alongside two potentially novel GPT-5.4 Pro optimizations, while expert review remains necessary.
- HorizonMath contains over 100 predominantly unsolved problems from applied mathematics, physics, and computer science, designed for high-probability automatic verification.
- The framework exploits a generator–verifier gap in closed-form discovery, discrete construction, and optimization tasks, making evaluation almost entirely computational.
- High-precision numerical comparison and deterministic checkers automate filtering, but matching a numerical reference does not formally prove an exact closed form.
- Current frontier models score near 0%, while GPT-5.4 Pro proposes two potentially novel optimizations, providing a reproducible signal of progress toward autonomous mathematical research.
- Future extensions would accept complexity-reducing simplifications and include proof-based problems integrated with formal systems such as Lean.
A Appendix
GPT-5.4 Pro produced novel optimizations for two solvability-1 problems, each beating the best-known baseline.
- Two solvability-1 problems received GPT-5.4 Pro optimizations that beat the best-known baseline.
A.1 Thin-Triangle Kakeya (128 slopes): Minimize Union Area
This benchmark evaluates a discrete, thickened Kakeya-type construction by minimizing the union area of 128 thin triangles. Its baseline comes from AlphaEvolve’s improved construction.
- The problem asks for a discrete thickened Kakeya-type construction with 128 equally spaced slopes and minimum union area.
- AlphaEvolve’s construction achieves union area ≈0.11481, improving on Keich’s earlier construction at ≈0.11921.
- The benchmark uses construction evaluation against the best-known published value and assigns solvability tier 1.
Thin-Triangle Kakeya (128 slopes): Minimize Union Area
The solution parameterizes 128 fixed-slope triangles by intercepts and searches for an arrangement minimizing their union area. Deterministic piecewise-linear integration validates the resulting construction against the AlphaEvolve baseline.
- Geometric construction: Each triangle is bounded above by ℓ_i and below by the segment from (0, b_i −δ) to (1, a_i + b_i), with a vertical edge closing it at x = 0.
- Result: Area(E) decreases from the AlphaEvolve best-known value ≈0.11481 to ≈0.10915, yielding a deterministic PASS verdict.
- Problem formulation: The 128 slopes are fixed at a_i = i/128, while the 128 intercepts b_0, b_1, …, b_127 are free parameters.
- Output: The output is a JSON object containing exactly 128 floating-point intercepts.
- Verification: The validator computes Area(E) deterministically by exact piecewise-linear integration of the union’s vertical cross-sections.
- Optimization: The optimization performs hierarchical local search over a dyadic basis after selecting structured seeds and globally optimizing level weights.
A.2 Asymptotic Upper Bound Constant for Diagonal Ramsey Numbers
This problem seeks to reduce the best-known exponential upper-bound base for diagonal Ramsey numbers below c ≈3.7992 by optimizing a correction function within the Gupta–Ndiaye–Norin–Wei framework. GPT-5.4 Pro produced two valid candidate solutions, achieving c ≈3.7296 and c ≈3.6961, both pending third-party verification.
- Problem: The task minimizes the upper-bound base c in R(k, k) ≤ c^k+o(k), improving on the current c ≈3.7992.The optimization replaces the existing correction with a polynomial-based ansatz whose sufficient conditions must hold across the required domain.
- Results: GPT-5.4 Pro supplied two different solutions for the optimization problem.One solution includes an explicit search function, while the other returns a valid quintic function without exposing its exact search procedure.
- Results: c ≈3.7296 was achieved by a valid quartic correction with coefficients [−0.32, 0.28, −0.025, −0.12525 . . .].This candidate includes an explicit search function.
- Verification: The candidate certificates verify all three sufficient conditions with strictly positive margin across every subinterval, including an analytic check when λ < 10−3.The validation also uses a symmetric R0 check that accepts either orientation of a pair.