Research Math Problems and Verifier-Backed Tasks for Frontier Models

Mathematical AI has a data problem.

Public benchmarks remain useful, but the strongest models increasingly know their distributions: the problem styles are familiar, solutions are searchable, and variants appear throughout public training corpora. A high score can show competence on a known benchmark without telling a model team how the system will behave on genuinely new mathematics.

The next generation of mathematical models needs a different kind of data:

• new problems that are difficult to solve through recall;
• tasks that expose research behavior rather than only final-answer accuracy;
• verifiers that turn difficult discoveries into reliable rewards;
• solving traces that preserve useful partial progress and informative failures;
• and private holdouts that remain outside the training pipeline.

Ulam now offers research-level mathematics problems, verifier-backed tasks, and solving trajectories through both off-the-shelf data packs and custom generation programs.

These products are complementary. Verifier-backed tasks provide scalable rewards. Open-ended research problems measure capabilities that cannot always be reduced to a binary answer: mathematical taste, obstruction finding, theorem selection, counterexample search, proof hygiene, and knowing when a promising argument is still incomplete.

Forcing every research question into a binary verifier destroys valuable signal. Leaving every task to unconstrained subjective grading makes evaluation difficult to scale. A useful research-mathematics program needs both.

Our open-ended research problems are closest in spirit to ErdosBench.

They range from difficult variants of known conjectures to new human- or AI-assisted research candidates. The statement may be elementary, while the search space demands graduate- or research-level mathematics. Typical objectives include:

• proving or disproving a conjecture;
• finding the decisive obstruction or counterexample;
• establishing a new special case;
• improving a quantitative bound;
• reducing the question to a better-understood theorem;
• or identifying exactly why an attractive proof strategy fails.

Examples of the mathematical flavor can be found in our note on ten new Erdős-style problems in number theory and combinatorics. The problems include extremal questions involving coprimality, gcd and lcm patterns, squarefree sums, additive configurations, and arithmetic graphs.

Many such problems are genuinely open-ended. There may be no known complete solution and therefore no honest final-answer verifier.

That does not mean the resulting data is ungradable.

A research-problem delivery can include a provenance and novelty-risk report, neighboring literature, elementary bounds, known special cases, computational experiments, model trajectories, expert assessments, and a structured account of what each trajectory actually establishes.

Instead of labeling a polished response “correct” or “incorrect” as a whole, we can separate:

• claims that are proved;
• claims supported only by computation;
• plausible conjectures;
• theorem applications whose hypotheses have been checked;
• reductions that are valid but incomplete;
• false steps;
• and the first unresolved proof obligation.

This produces a much richer signal than a raw model transcript.

A lightweight problem pack may include two independent model rollouts. Deeper programs can use configurable best-of-(k) sampling across models, prompts, inference budgets, or tool configurations.

For open-ended mathematics, however, “best” should not mean “the most confident answer.”

A useful two-trajectory delivery is often:

1. the strongest expert-rated attempt, preserving every verified lemma or meaningful reduction; and
2. the most informative near-miss, annotated at the first material error or unsupported jump.

The result can be transformed into several training views:

• a positive partial-progress trajectory;
• a first-bad-step detection example;
• a critique of an invalid theorem application;
• a repaired continuation that preserves the valid prefix;
• a preference pair contrasting calibrated progress with an overclaimed solution;
• or a research-planning example showing which direction should be explored next.

Longer campaigns can also retain negative attempts, counterexample searches, code executions, literature queries, revisions, and disagreements between models or reviewers.

A hard prompt is not yet a dataset. A fluent answer is not yet a solution. The value lies in identifying which parts of the reasoning survive scrutiny.

The second product class consists of research-level tasks with objectively checkable outcomes.

These tasks preserve much of the depth of mathematical research while ending in an answer, construction, or certificate that can be verified automatically. They are particularly suitable for RLVR and self-contained reinforcement-learning environments.

Examples include:

• determining an extremal quantity for a bounded instance;
• constructing a graph, code, sequence, or combinatorial object with specified properties;
• finding a counterexample within a large search space;
• optimizing a mathematical construction;
• computing an exact invariant;
• proving a finite case through a machine-checkable certificate;
• or solving a computational proxy derived from an open conjecture.

The task may be extremely difficult for a model to solve, while the resulting object can be checked quickly.

A verifier-backed delivery can include:

• the problem statement and answer contract;
• an executable verifier or certificate checker;
• private and adversarial test cases;
• reference outputs or witness objects;
• timeout and numerical-tolerance rules;
• reward-hacking tests;
• scored model trajectories;
• stable task IDs and versioned manifests;
• and optional Lean 4 formalization where appropriate.

The verifier boundary is stated explicitly. A Python checker establishes that a submitted object satisfies a finite property; it does not automatically prove the corresponding asymptotic conjecture. A numerical experiment provides evidence; it is not a theorem. A Lean-accepted statement is formally verified only at the scope encoded in Lean.

This distinction is essential for trustworthy RLVR data.

One open problem can generate several complementary tasks.

A source conjecture may produce:

• a literature and novelty-triage task;
• a proof-gap detection task built from a plausible but invalid argument;
• an exact finite-proxy task;
• a counterexample-search environment;
• a theorem-selection task;
• a research-planning prompt;
• and a longer research-progress episode.

This family structure is useful for both training and evaluation. A model can first learn to solve bounded instances, then identify proof gaps, then attempt the open-ended source question. The difficulty can be adjusted without changing the underlying mathematical concepts.

It also makes contamination control more important. Train, development, and holdout splits should be separated at the problem-family level—not merely by changing constants or rewriting the statement.

Ulam maintains UnsolvedMath.com, a continuously expanding archive of more than 8,000 open, partially solved, and historically significant mathematical problems.

The corresponding UnsolvedMath dataset on Hugging Face provides a machine-readable view of the collection, with mathematical statements, source provenance, domain labels, difficulty information, and research notes.

The archive spans major areas of mathematics and brings together problems from sources such as Erdős problem collections, AIM workshops, AMR open-problem lists, the Kourovka Notebook, low-dimensional topology problem lists, and major historical challenge sets.

UnsolvedMath is not itself a private benchmark: its public statements can be present in model training data. It serves a different role.

It is our map of the problem landscape.

We use it to identify underexplored domains, track problem status, locate neighboring results, design bounded proxies, build new variants, and find research structures that can be transformed into private task families. Public source provenance is retained, while custom evaluation statements, answers, verifiers, and holdout variants can remain protected.

For new human-posed or synthetic research candidates, we distinguish carefully between:

• a known problem or direct restatement;
• a variant of an existing question;
• a candidate with no exact match found in a defined search;
• and a specialist-vetted open problem.

“No exact match found” is not treated as a formal proof of novelty. Status labels, search scope, and uncertainty should be part of the data.

Problems and verifiers are only part of the product. The path between them contains many of the most valuable training signals.

A full research trajectory may show a model:

• proposing several approaches;
• discarding a false analogy;
• running a finite experiment;
• discovering an invariant;
• applying a theorem under the wrong assumptions;
• receiving a verifier failure;
• repairing the construction;
• proving a useful local lemma;
• and stopping with an honest statement of what remains open.

These records can support supervised fine-tuning, critic training, proof repair, process supervision, preference optimization, and RLVR.

Our Verified Research Reasoning Trajectories work converts human mathematician–AI research conversations into structured reasoning data. Rather than applying one blanket “verified” label to an entire transcript, the data records the verification status and dependencies of smaller proof or reasoning units.

We also build ArxivNet, which transforms more than 5,000 mathematics papers into structured proof-process data for theorem dependencies, reconstruction, critics, preferences, negative traces, and long-context mathematical training.

Results from our post-training experiments are available through the Ulam scorecards.

The intended use determines what should be delivered.

Once a model has been trained on a task’s statement, solution trace, or verifier, that exact item should not be presented as evidence of generalization.

For programs that need both training and continuing evaluation, we recommend a family-disjoint split with a rolling holdout. Retired holdout items can later be released for training and replaced with newly generated families.

This creates a continuous loop:

problem → attempt → verifier or expert verdict → first failure → critique and repair → training export → refreshed evaluation

Research-mathematics programs can be customized by:

• mathematical domain and subfield;
• graduate, PhD, or open-research difficulty;
• open-ended versus verifier-backed composition;
• required verifier coverage;
• number and source of model trajectories;
• inference and tool-use budgets;
• expert-review depth;
• novelty and literature-audit requirements;
• optional Lean formalization;
• training, evaluation, or combined usage;
• and JSONL, Parquet, repository, API, or hosted-runner delivery.

For an initial custom program, Ulam can currently support approximately 1,000 accepted research problems or tasks, depending on the verifier, formalization, and expert-review requirements.

Larger programs can be expanded through phased delivery toward approximately 10,000 items, with calibration and quality gates established before scaling.

A typical engagement begins with a representative pilot across several subjects and task types. The pilot fixes the schema, difficulty definition, verifier contract, model-sampling budget, acceptance criteria, and review protocol. Production then proceeds in audited batches rather than as one undifferentiated task dump.

Frontier mathematical reasoning is not one capability.

It includes exact calculation, proof construction, counterexample search, theorem retrieval, literature judgment, code use, self-correction, formalization, and the ability to distinguish a promising direction from a finished result.

Research Math Problems test how a model behaves when the answer is not known.

Research Math Tasks turn difficult mathematical discoveries into scalable, verifier-backed rewards.

Research Reasoning Datasets preserve the successful steps, failed approaches, critiques, and repairs that connect the two.

Ulam offers all three as off-the-shelf data products and custom programs for teams building mathematical reasoning models, theorem provers, research agents, and frontier evaluation systems.

Train on harder mathematics. Measure progress on problems the model has not already seen. Preserve the verification boundary.