HorizonMath: Testing AI's Ability to Discover New Mathematics

Paper: 2603.15617 Authors: Erik Y. Wang, Sumeet Motwani, James V. Roggeveen, Eliot Hodges, Dulhan Jayalath, Charles London, Kalyan Ramakrishnan, Flaviu Cipcigan, Philip Torr, Alessandro Abate Categories: cs.LG

The Gap

Existing AI math benchmarks test known problems with known solutions. MATH, GSM8K, and similar datasets measure reasoning ability, but they’re vulnerable to data contamination—models might have seen the answers during training. Formal proof benchmarks like Lean require expensive human verification or theorem provers that don’t scale. We can measure if AI can solve undergraduate calculus, but we can’t measure if AI can do actual mathematical research.

The boundary: we have no scalable way to test whether AI can make novel mathematical discoveries. Prior work either uses solved problems (contamination risk) or requires manual expert review (doesn’t scale).

Problem: Can AI discover new math?
    |
    v
Existing approaches fail:
    |
    +---> Known problems: Data contamination risk
    |
    +---> Formal proofs: Expensive verification
    |
    v
This paper's insight: Target problems where
    - Discovery is hard (requires insight)
    - Verification is easy (automatic)
    |
    v
Method: HorizonMath benchmark
    - 100+ unsolved problems
    - Automated verification
    - 8 computational math domains
    |
    v
Evidence: Models score ~0%, but GPT-4 found
          2 potential novel results
    |
    v
Conclusion: First scalable benchmark for
            mathematical discovery capability

The Increment

One sentence: Before this paper, we couldn’t systematically test AI’s ability to discover new mathematics at scale; after it, we have a benchmark of real unsolved problems with automatic verification where solutions could be publishable results.

Core Mechanism

HorizonMath consists of three components working together. First, a curated problem set of 100+ unsolved problems across 8 domains (optimization, graph theory, combinatorics, number theory, etc.). These aren’t arbitrary puzzles—they’re problems where the mathematical community doesn’t know the answer, but where proposed solutions can be verified computationally.

Second, an automated verification framework. Each problem comes with a verification function that can check if a proposed solution is correct. For example, if the problem asks for the minimum value of some function, the verifier can evaluate the function at the proposed point and check constraints. This is the key innovation: the problems are chosen specifically because verification is cheap even though discovery is hard.

Third, a standardized evaluation protocol. Models are given problem statements and must output solutions in a structured format. The framework runs the verification automatically, tracks which problems are solved, and maintains a leaderboard. When a model proposes a solution that passes verification and improves on known bounds, it flags this as a potential novel contribution requiring expert review.

Problem Database                 AI Model
    |                               |
    v                               v
[Unsolved Problem] ---------> [Generate Solution]
    |                               |
    | (includes verification        |
    |  function)                    v
    |                          [Proposed Answer]
    |                               |
    v                               v
[Verification Function] <----- [Submit Solution]
    |
    v
Check: Is solution valid?
    |
    +---> Yes: Score point
    |     |
    |     v
    |     Better than known bound?
    |     |
    |     +---> Yes: Flag for expert review
    |     |          (potential novel result)
    |     |
    |     +---> No: Just a correct solution
    |
    +---> No: Score 0

Think of HorizonMath like a climbing gym for AI researchers. The gym has 100+ routes (problems) that no one has completed yet. Each route has a sensor at the top (verification function) that automatically detects if you reached the summit correctly—no human judge needed. The routes are designed so that getting to the top requires real climbing skill (mathematical insight), but once you’re there, the sensor can instantly verify you made it (computational check). Most climbers (current AI models) can’t complete any routes. But occasionally, someone finds a new path to the top that’s better than any known route—that’s a potential breakthrough worth having experts examine. The gym stays relevant because the routes are genuinely unsolved, and new routes can be added as the community discovers them.

Key Concepts

• Discovery-hard, verification-easy problems: This is the sweet spot HorizonMath targets. Imagine you’re trying to pack circles into a square as tightly as possible. Finding the optimal packing requires deep geometric insight—you might need to try thousands of configurations, use symmetry arguments, or have a creative breakthrough. But once someone shows you a packing, verifying it’s valid is trivial: just check that no circles overlap and all fit inside the square. You can even compute the packing density automatically. This asymmetry—hard to find, easy to check—is what makes these problems perfect for automated benchmarking. It’s like Sudoku: solving is hard, but checking a solution takes seconds.

• Data contamination immunity: Current benchmarks have a fatal flaw. If you train a language model on the entire internet, and the internet contains the answer to “What is 2+2?”, the model might just memorize “4” rather than learn addition. With HorizonMath, the answers literally don’t exist in any training data because they’re unsolved problems. It’s like testing a student’s creativity by asking them to write a story that’s never been written before—you know they can’t have memorized it. This makes the benchmark future-proof: even as models train on more data, they can’t cheat by memorization.

• Computational mathematics domain: Not all math is created equal for this benchmark. HorizonMath focuses on computational and applied mathematics—areas where problems have numerical or algorithmic answers that can be verified by running code. This excludes pure mathematics where verification requires formal proofs (too expensive to automate) or subjective judgment (not scalable). Think of it as the difference between “find the shortest path through these 100 cities” (computational—you can verify by measuring the path length) versus “prove the Riemann hypothesis” (pure—requires human mathematicians to verify the logical argument). The benchmark lives in the computational zone where automation is possible.

Framework Shift

Before (mainstream approach):        After (this paper):

Known Problems                       Unsolved Problems
    |                                    |
    v                                    v
[Train on solutions] ------>        [No solutions exist]
    |                                    |
    v                                    v
Test on held-out                    Test on real open
known problems                      problems
    |                                    |
    v                                    v
Risk: Data contamination            Immune: Can't memorize
      Model may have seen                 what doesn't exist
      answers                             |
    |                                    v
    v                                Verification:
Verification:                       Automated (cheap)
Manual or formal proof              
(expensive)                         Discovery:
                                    Requires insight
Measures: Reasoning                 
          on known math             Measures: Research
                                              capability

From testing if AI can solve textbook problems to testing if AI can discover new mathematics, the core shift is moving from evaluation on known answers to evaluation on unknown frontiers.

Expert Assessment

Problem choice: This is a real gap, not manufactured. The field has been stuck measuring AI on undergraduate-level math while claiming models can “reason.” The jump to research-level capability is the actual frontier, and this paper targets it directly. The timing is right—models are getting good enough that this question matters. The choice to focus on computational math is pragmatic and honest about what’s automatable.

Method maturity: This is more infrastructure than algorithmic innovation, and that’s fine—the field needs good benchmarks. The “discovery-hard, verification-easy” criterion is clever and well-executed. However, the paper doesn’t deeply explore why current models fail. Are they missing mathematical intuition, search strategies, or something else? The two potential novel results from GPT-4 are tantalizing but need expert confirmation—the paper is appropriately cautious here.

Experimental integrity: The baseline results are sobering—most models score near 0%, which validates that these are genuinely hard problems. The paper is transparent about the two potential discoveries being unverified. One concern: the problem selection process isn’t fully detailed. How were these 100+ problems chosen? Are they representative of mathematical research, or cherry-picked for verifiability? The paper would benefit from more discussion of problem curation methodology.

Writing quality: The paper is clear and well-structured, but the related work section undersells the novelty. The authors spend too much time comparing to formal proof benchmarks when the real contribution is the unsolved problem + automated verification combination. The experimental section could be tighter—some results feel like “we ran the models and they failed,” which is expected. More analysis of failure modes would add value.

Verdict: Strong accept — This is infrastructure the field needs, executed competently with appropriate caution about claims.

Takeaways

The “discovery-hard, verification-easy” framework transfers beyond mathematics. If you’re building benchmarks for any domain, look for problems where generating solutions requires creativity or insight, but checking solutions is mechanical. This asymmetry enables scalable evaluation without human judges. Examples: protein folding (hard to design, easy to simulate stability), algorithm optimization (hard to find, easy to benchmark performance), or even creative writing with constraint satisfaction (hard to write, easy to check constraints).

The data contamination immunity strategy is generalizable: use problems with unknown answers. For code generation, this means testing on newly released APIs or frameworks. For scientific reasoning, use recent preprints or ongoing research questions. The benchmark stays fresh because the frontier keeps moving.

The paper’s honesty about unverified discoveries is a model for AI research. When you find something that might be novel, flag it clearly and call for expert review rather than overclaiming. This builds trust and invites collaboration with domain experts.