ULAM / ULAMGYM
Private alpha / 1 task Discuss access ↗
Private research environment · one task

// Long-horizon mathematical RL

Can a model know when a proof is actually finished?

UlamGym is built from manually hand-crafted, research-level mathematics tasks. The first task is private and intentionally long-horizon. In internal attempts, multiple frontier models have announced a solution—then retracted it when later checks exposed a gap.

Discuss private access See the research episode ↓
Tasks today1 private task
ConstructionHand-crafted
HorizonResearch-scale
Primary signalClaim → check → revise
Task creationManualDesigned by hand, not mass-generated.
DifficultyResearch-levelLong dependency chains and unresolved uncertainty.
EpisodePersistentProof state, checks, and retractions survive across steps.
AnalysisError-centricStudy why a plausible proof became an invalid one.

// 01

Not another answer-only math benchmark.

UlamGym is designed around the part of mathematics that short-form evaluations erase: building a research plan, tracking dependencies, challenging one’s own lemmas, revising after contradictions, and knowing when confidence has outrun evidence.

THE UNIT OF EVALUATION IS
A RESEARCH TRAJECTORY.

Conventional math evaluation

Answer-level
→Model receives a compact problem
→Model emits one proof or numerical answer
→A grader marks the final artifact

Useful for local competence. It often hides whether the model noticed its own gaps, tested fragile steps, repaired a failed line of reasoning, or simply stopped when the prose looked complete.

UlamGym

Research-level
→Build a persistent map of definitions, lemmas, cases, and open obligations
→Make claims, attack them, and preserve the evidence behind every revision
→Finish with a verified proof—or a calibrated account of what remains open

The environment makes premature closure, circularity, hidden assumptions, self-correction, and uncertainty management visible as first-class research behavior.

// 02

The proof search is the environment.

A UlamGym episode maintains a durable research state. The policy decides what to formalize, which branch to pursue, what deserves verification, when to challenge a result, and whether a claimed solution should survive another round of scrutiny.

ORIENT → CONJECTURE → PROVE
→ AUDIT → REVISE.

Stage 01 / research map

Turn a hard statement into an explicit field of obligations.

The model identifies definitions, equivalent formulations, limiting cases, plausible invariants, known tools, and the parts of the statement that are most likely to conceal a trap.

ArtifactProblem mapDefinitions, subclaims, dependencies, edge cases, and unresolved questions.
DecisionAttack surfaceWhich bottleneck would collapse the largest portion of the search tree?
ControlScope disciplineSeparate proved facts, imported facts, conjectures, and analogies.
RiskFalse familiarityDetect when a hard research problem merely resembles a standard exercise.

// 03

One task. Kept private on purpose.

The current UlamGym task is not publicly disclosed. Its value depends on preserving the statement, task-specific probes, expert annotations, and the history of model attempts as a controlled research surface.

NO PUBLIC STATEMENT.
NO PUBLIC LEADERBOARD.

UG-001Private · active

The first UlamGym problem.

A manually constructed, long-horizon mathematics task designed to force deep dependency management rather than fast pattern completion. The public page does not reveal its statement, field, organizer knowledge state, or the details of prior model attempts.

Objective
Produce a research-grade resolution whose dependencies survive adversarial review.
Episode state
Persistent notebook, claim ledger, dependency graph, checks, counterexamples, and revisions.
Interesting behavior
Frontier models have reached high-confidence “solutions” and later withdrawn them.
Evaluation
Structured checks, task-specific probes, proof review, and a record of the full reasoning trajectory.
Publication
Not public. Results and traces are shared only under a controlled research agreement.
Success
A proof that survives verification—or a precise, calibrated account of what remains unresolved.
Why only one? Research-grade tasks are expensive to author and harder to evaluate than short-answer benchmarks. UlamGym favors depth, provenance, and failure analysis over task count.

// 04

The interesting data begins where the proof breaks.

When a model retracts a solution, UlamGym does not reduce the episode to zero. It asks what kind of mistake occurred, when it became detectable, whether the model found it itself, and whether the revision improved the research state.

ERRORS ARE TRAJECTORIES.
NOT JUST LABELS.

// 05

The reward is not confidence.

UlamGym is intended to reward verified mathematical progress, useful error localization, productive revision, and calibrated stopping—while penalizing unsupported closure and repeated dependence on invalid steps.

CONCEPTUAL REWARD DESIGN.
PRIVATE SPEC EVOLVING.

Research-episode objective

Repisode = Δ verified frontier + recovery + calibration − unsupported closure − repeated invalidity

A model can make valuable progress without solving the full problem: proving a reusable lemma, finding a decisive counterexample, isolating a minimal invalid core, or correctly retracting an overclaim can all improve the research state. The private scoring protocol remains task-specific.

01
Verified frontierWhich claims survive task-specific checks and expert review?
progress
02
Error localizationHow precisely is the failing dependency identified?
diagnosis
03
Recovery qualityDoes the next branch preserve valid work and change strategy?
revision
04
Epistemic calibrationDoes confidence track the actual verification state?
belief
05
Research efficiencyUseful progress per token, tool call, check, and wall-clock step.
cost

// 06

The model sees the problem. Ulam preserves the evaluation boundary.

The research policy operates through a persistent task session. Ulam controls the private statement distribution, task-specific checks, expert annotations, evaluation rubric, and the final interpretation of what the trajectory establishes.

A PRIVATE RESEARCH ENVIRONMENT.
NOT AN OPEN LEADERBOARD.

Visible to the research policy

  • The task statement, definitions, and permitted mathematical tools
  • A persistent notebook and explicit claim/dependency state
  • Results from allowed local checks and requested probes
  • Previously verified lemmas, failed branches, and retractions
  • Remaining compute, token, tool, and wall-clock budget
  • Structured feedback suitable for continued research

Sealed by Ulam

  • The public release decision and full task authoring history
  • Expert annotations, adversarial probes, and evaluation rubric
  • Prior model traces and known recurring failure patterns
  • Task-specific holdout checks and organizer-side audit notes
  • The status of any reference argument or unresolved organizer questions
  • Private cross-model forensic analysis and training-data derivatives

// Persistent research boundary

Lab-operated model
01Frontier model / research policyPinned model + scaffold
02UlamGym sessionState + budgets + receipts
03Research notebookClaims + dependencies + revisions
Structured checksAlgebra, domain, counterexample, dependency, and task-specific probes.
Expert auditResearch-level review for steps that cannot be reduced to a generic verifier.
Private task and evaluation stateThe statement, organizer notes, prior attempts, hidden probes, and cross-model comparison remain inside Ulam’s controlled research boundary.

// 07

Built for the edge cases that easier benchmarks miss.

UlamGym focuses on situations where a model can be locally impressive, globally wrong, and uncertain about the difference. The environment is intentionally small, expensive, and diagnostic.

DEPTH OVER VOLUME.
FORENSICS OVER A SINGLE SCORE.

Core

Manually authored

Every task is designed and reviewed as a research object rather than sampled from a template generator.

Core

Long-horizon state

The environment preserves research memory, abandoned branches, proof debt, and revisions across an extended episode.

Core

Claim provenance

Every conclusion can be traced back to the exact lemmas, checks, assumptions, and model actions that support it.

Core

Retraction-aware

A withdrawn claim is analyzed for timing, cause, completeness, calibration, and the quality of the next research move.

Core

Mixed verification

Structured probes and executable checks are combined with expert mathematical review where generic automation ends.

Core

No answer leakage

Private access, controlled traces, and no public leaderboard reduce contamination and repeated tuning to the task.

Core

Model forensics

Compare not only who “solves,” but how models form beliefs, defend weak steps, discover contradictions, and recover.

Core

Training-loop ready

Verified lemmas, invalid cores, counterexample episodes, and repaired trajectories can become targeted post-training assets.

// 08

Private access built around a research question.

UlamGym is not currently a public benchmark. Early work should freeze a model and scaffold, run controlled episodes on the private task, and close with a forensic comparison of claims, errors, retractions, and verified progress.

ONE TASK CAN STILL PRODUCE
A DEEP MODEL DIAGNOSIS.

01

Research question freeze

Choose the model, scaffold, tool policy, episode budget, assistance rules, and the behaviors the comparison is meant to distinguish.

Design
02

Controlled private runs

Execute independent long-horizon episodes from clean state while preserving every claim, check, revision, and resource event.

Run
03

Mathematical audit

Review the proof frontier, minimal invalid cores, retraction timing, surviving lemmas, confidence shifts, and repeated failure motifs.

Verify
04

Failure-to-training loop

Convert verified mistakes and productive recoveries into targeted data, critics, preferences, probes, or a refreshed task variant.

Learn

// 09

Evidence a research team can inspect.

The output is not just “solved” or “failed.” A UlamGym study can show where a model’s proof frontier advanced, why a solution claim collapsed, how uncertainty changed, and which behaviors are promising targets for post-training.

A RETRACTION CAN BE
MORE INFORMATIVE THAN A PASS.

01

Research trace

Chronological record of hypotheses, proof steps, checks, tool calls, claims, reversals, and stopping decisions.

02

Proof frontier

Verified lemmas, unresolved obligations, imported facts, heuristic steps, and the exact status of the final claim.

03

Dependency graph

Machine-inspectable support relationships that expose hidden assumptions, circularity, and proof debt.

04

Retraction map

When confidence peaked, what evidence reversed it, which components survived, and whether the correction generalized.

05

Calibration profile

Confidence versus verification state across lemmas, global claims, contradictions, and final stopping behavior.

06

Training candidates

Minimal invalid cores, repaired proof segments, counterexample searches, critic traces, and preference-ready comparisons.

Customer-safe output

A model-forensics artifact, not a public scorecard.

The report centers the pinned model setup, verified mathematical frontier, claim history, error taxonomy, calibration, resource use, and limitations. The private task statement and sensitive traces remain excluded unless explicitly agreed.

Private taskProof graphClaim ledgerRetraction traceCalibrationTraining candidates

// 10

Questions research teams ask first.

The current program is intentionally explicit about what exists today, what remains private, and what a result would—and would not—show.

ONE PRIVATE TASK TODAY.
MORE ONLY WHEN THEY ARE READY.

Is the current UlamGym task public?

No. The statement, mathematical domain, organizer notes, task-specific checks, and prior model traces are private. This prevents contamination and preserves the value of the task as a controlled research surface.

Why build a gym around only one task?

UlamGym currently contains one private task, while we hand-craft additional research-level tasks. These are not interchangeable benchmark rows: a single carefully authored problem can support many long-horizon episodes, model comparisons, failure analyses, verifier refinements, and training loops. The design goal is depth and diagnostic value, not catalog size.

Do model retractions count as failure?

A retracted solution is not a solved task, but the retraction itself can be a positive research behavior. UlamGym distinguishes early self-correction, late correction, external correction, incomplete correction, and doubling down after contradictory evidence.

What counts as success?

A research-grade resolution whose dependencies survive the private evaluation process. Depending on the task and organizer state, a rigorous partial result or a precise explanation of the remaining obstruction may also be valuable—but unsupported confidence is never equivalent to a proof.

Is UlamGym a formal theorem-proving benchmark?

Not exclusively. Structured and executable checks are used wherever possible, but research mathematics often exceeds the coverage of a single proof assistant or generic verifier. The environment combines explicit proof-state structure, task-specific probes, and expert review.

Can the traces be used for post-training?

Yes, under an agreed data-use scope. Verified lemmas, counterexample searches, minimal invalid cores, repaired arguments, confidence corrections, and critic comparisons can become SFT, preference, verifier, or RL signals.

Does a strong result prove human-level mathematical research?

No single private task can establish broad human-level research ability. It can provide unusually deep evidence about one model’s proof search, self-verification, epistemic calibration, recovery, and behavior on an ultra-hard task near the edge of current capability.

// UlamGym private research

One problem can expose an entire model’s epistemology.

Bring a frontier model, a frozen scaffold, and a precise question about mathematical reasoning. Ulam will operate the private task, preserve the full research trace, audit the proof frontier, and turn the failures into the next training opportunity.

Discuss private access ↗