One-sentence Summary

Researchers at ulam.ai introduce the UnsolvedMath dataset as a research-level mathematical reasoning benchmark and evaluate GPT-5.2, Gemini 3 Pro, Grok, and Opus 4.5 on literature search, theorem proving, proof checking, and formalization, finding that none can autoformalize, that GPT-5.2 Extended Thinking performs at PhD-student level on simpler problems, and that extended thinking time is the primary driver of reasoning quality while global mental picture, systematic self-verification, and analogical reasoning remain absent.

Key Contributions

• Introduces the UnsolvedMath dataset, a public benchmark that structures open mathematical problems into evaluation episodes with retrieved lemmas, verifiable subgoals, deterministic tests, and proof-assistant checks.
• Defines a four-dimension evaluation protocol covering literature search, theorem proving, proof checking, and formalization, and applies it to GPT-5.2, Gemini 3 Pro, Grok, and Opus 4.5; results show strong literature search, no autoformalization, PhD-student-level performance by GPT-5.2 Extended Thinking on simpler problems, and extended thinking time as the primary driver of reasoning quality.
• Identifies absent capabilities in global mental picture, systematic self-verification, and analogical reasoning, supports a human-AI collaborative paradigm with the Erdős #728 proof, and proposes analogy prompts to separate coached reasoning from autonomous insight.

Introduction

The authors address the challenge of evaluating large language models on open mathematical problems, where confident fabrication can produce plausible proofs with invented lemmas or circular reasoning, especially for non-expert users. They highlight mathematics as an ideal testbed because formal proof assistants provide objective ground truth, and they argue that verification must be built into the workflow rather than treated as optional. Prior evaluations tend to use single difficulty scores, overlook behavioral effects such as models refusing problems labeled "open," and do not separate literature search, constructive reasoning, and critical reasoning. The authors contribute an UnsolvedMath-based episode protocol with verifiable subgoals, deterministic algebraic and numeric checks, proof-assistant fragments, injected flawed proofs for detection testing, and a multidimensional scoring rubric for search, proof generation, verification, and formalization.

Method

The evaluation framework treats each UnsolvedMath entry as a benchmark seed rather than a static prompt. For each seed, the authors derive three components: a short-context version of the problem statement, a set of related known lemmas or results that can be retrieved, and a collection of verifiable subgoals such as toy cases, parameter regimes, or literature lemmas. This decomposition supports evaluation of both final theorem proving and the intermediate research process.

Each model run is structured as an episode with a fixed tool and time budget. An episode includes literature search, a proposed approach, intermediate lemma attempts, a proof check of the model's own output, and optional formalization. The budget is intended to enable fair comparison across systems while reflecting a bounded research session.

The verification layer is central to the protocol. Subgoals are checked through deterministic tests, including algebraic identities, numerics, and finite cases, as well as proof-assistant fragments where applicable. Proof-check items also include injected flawed proofs to measure whether a model can detect errors. This layer is designed to reduce the risk of confident fabrication, in which a model generates a plausible-looking proof with invented lemmas, circular reasoning, or fictitious references. The authors recommend pairing open-problem episodes with verification layers and explicit uncertainty quantification, particularly for users without specialist mathematical training.

Scoring is multidimensional. Literature search is scored on a 0 to 5 scale, proof-check on a 0 to 5 scale, and formalization on a 0 or 1 scale. Proving is scored on a 0 to 5 scale based on the number and difficulty of verified subgoals, with additional credit for generalization beyond retrieved templates. This rubric separates search and synthesis, constructive reasoning, and critical reasoning, reflecting the fact that problem difficulty can arise from a missing conceptual insight, from long technical chains, or from both.

Prompt framing is also treated as part of the protocol. Models often perform worse or refuse entirely when a problem is labeled as open, apparently due to excessive caution or learned helplessness. To address this, the evaluation removes such labels or provides candidate strategies for the model to evaluate. The framing "test whether this approach works" consistently outperforms "solve this open problem." This design choice distinguishes autonomous reasoning from coached reasoning and helps measure how much model performance depends on human steering.

Experiment

Best models now perform near or above human baselines on several standard and competition-level benchmarks, including GSM8K, MATH, AIME 2025, and GPQA Diamond. In contrast, FrontierMath and PutnamBench still show considerably lower scores, indicating that harder research-level mathematical reasoning remains challenging. Models have reached near-saturated performance on GSM8K, MATH, and AIME 2025, and surpass the provided PhD baseline on GPQA Diamond. Research-level benchmarks show the largest remaining gaps: FrontierMath reaches only 40.3% and PutnamBench reaches 70.0%.

Across the evaluated frontier models, mathematical reasoning capabilities vary sharply by task. All models excel at literature search, but none can produce machine-verifiable Lean formalizations. GPT-5.2 shows the strongest theorem-proving performance, while Grok is comparatively better at proof checking. All models achieve the maximum literature search score, indicating consistent strength in retrieving and synthesizing relevant prior art. No model produces machine-verifiable Lean code, revealing a shared gap in formalization. GPT-5.2 leads in theorem proving, followed by Grok, while Gemini 3 Pro and Opus 4.5 trail closely behind. Grok is the strongest at identifying major gaps or invalid steps in proposed proofs, whereas the other models score notably lower.

The first evaluation compares frontier models against human baselines on standard and competition mathematics benchmarks, showing saturated performance on widely used datasets while research-level benchmarks such as FrontierMath and PutnamBench still expose significant gaps. The second experiment tests task-specific mathematical abilities, finding that all models consistently excel at literature search but cannot produce machine-verifiable Lean formalizations, with GPT-5.2 strongest in theorem proving and Grok strongest in proof checking.