数学 Harness 的
设计与实验

许超 Chao Xu, 电子科技大学, 2026.9.19

Models are strong at research-level mathematics

MathArena ArXivMath leaderboard for 08/2026: GPT-6 Astra (max) 88.60% accuracy at $3.63 per problem, Claude-Fable-5.1 (high) 87.72% at $12.77, Qwen3.8-Max 57.89% at $5.76, Muse Spark 1.3 45.61%, Gemini 3.8 Flash 40.35%, Kimi K3 (Think) 38.60%. Per-problem cells colored by correctness.
MathArena

FrontierMath Tier 4: saturated

Epoch AI chart: FrontierMath Tier 4 accuracy against release date, 2025 to 2026, rising from under 10% to a highest score of 98%.
Epoch AI
What is left for us to do?
2019 2020 2021 2022 2023 2024 2025 2026 $100k $1M $10M $100M $1B publication date training compute cost, 2023 dollars, log scale OpenAI Five, $4M, 2019 GPT-3 175BGPT-3 175B (davinci), $2M, 2020 Wu Dao 2.0, $3M, 2021 Megatron-Turing NLG 530B, $4M, 2021 EXAONE 1.0, $3M, 2021 GPT-3.5 (davinci-002), $5M, 2022 PaLM (540B)PaLM (540B), $3M, 2022 GPT-4 (Mar 2023), $37M, 2023 SenseChat, $5M, 2023 PaLM 2, $5M, 2023 Claude 2, $5M, 2023 Falcon-180B, $11M, 2023 Amazon Titan, $8M, 2023 Inflection-2, $13M, 2023 Gemini 1.0 UltraGemini 1.0 Ultra, $31M, 2023 Nemotron-4 340B, $21M, 2024 Claude 3.5 SonnetClaude 3.5 Sonnet, $26M, 2024 Llama 3.1 405BLlama 3.1-405B, $53M, 2024 Grok-2, $32M, 2024 Grok 3Grok 3, $218M, 2025 GPT-4.5GPT-4.5, $366M, 2025 Llama 4 Behemoth (preview), $45M, 2025 Grok 4Grok 4, $388M, 2025
train a model
3.5× more expensive every year since 2020
frontier labs have raised over $370 billion
Epoch AI
Models one-shot hard problems.
Some problems no single shot solves.
That is where the harness comes in.
Solve more problems.
capability: the class of problems solved
Cheaper.
cost: money, sometimes time

More compute, more solved problems

OpenAI's September 2026 chart data: pass rate rises from 8.4% to 17.0% for GPT-6 Astra and from 26.2% to 47.4% for its internal model as test-time compute increases. Logarithmic compute axis and standard-error bars.
OpenAI
Likely: OpenAI has a mathreasoning harness
1 h 2 h 4 h 8 h 16 h $10 $100 $1,000 time cost Codex-goal$19, 1.4 h ProofCouncil$29, 2.1 h Rethlas$61, 1.8 h QED$71, 7.0 h Danus*$1,979, 12.1 h Xean$9, 1.7 h
*Danus at 12 h
Why the big gap?
Background:
how these AI things work
Edward Lockhart

Model

probability distribution tokens sample next token append, repeat sequence of tokens tokens tokens a single call the loop, packaged

The model is memoryless. The context has a length limit.

token — the unit of text, roughly a word, you pay per token

prompt — the part of the model input you control, context — the entire model input

GPT-6 Astra, Fable 5.1, Gemini 3.1 Pro, open weights: Qwen 3.8, DeepSeek-V4, Kimi 3, GLM-5.2, Gemma 4

This talk: GPT-6 Astra

How does the model "think"?

message thinking … pages of it reply hidden from you — closed models never release it you see this "thinking" = part of the output, not shown you toggle how much: effort low, medium, high, xhigh, Pro

What a harness adds

Context management
A memoryless model receives context kept by the harness and returns new output. Two objects linked by arrows.
Environment interaction
The model acts on the environment through tools and receives results. Two objects linked by arrows.
AGENT = MODEL + HARNESS

Doing mathematics with AI

Verification
A single checkmark representing verification.
Exploration
An unlabeled branching tree representing exploration.
Xean’s design
1. Maximize reasoning
2. Trust the model
3. Verify independently
4. Minimize cost
5. Survive interruptions
1. Maximize reasoning
where the money went, and why

Reasoning is the problem

OpenAI built reasoning models. Math fell out.
Noam Brown
“In mathematics, you’re purely bottlenecked by thinking … and the models are really good at that.”
Models “can think for weeks when scaffolded reasonably well.”

Same problem, same model

1 h 2 h 4 h 8 h 16 h $10 $100 $1,000 time cost Codex-goal$19, 1.4 h ProofCouncil$29, 2.1 h Rethlas$61, 1.8 h QED$71, 7.0 h Danus*$1,979, 12.1 h Xean$9, 1.7 h
*Danus at 12 h

Where a token sits sets its price

cached prefix fresh input reasoning reply 1, first write 12.5 10 output 50
cachedresend an exact recent prefix cache writepaid once, to store cache life30 minutes, sometimes longer
GPT-6 Astra, $1 / $10 / $12.50 / $50 per 1M

Where our inference budget went

reasoning visible output fresh input cached input Codex-goal 24% 10% 20% 45% ProofCouncil 31% 12% 16% 41% Rethlas 23% 34% 35% QED 19% 17% 25% 38% Danus* 14% 34% 45% Xean 68% 21%
Reasoning is 14 to 31% of cost in five systems, 68% in Xean.
*Danus at 12 h

Conversation cost is quadratic

every turn re-sends the whole transcript, reasoning included
turn 1 turn 2 turn 3 turn 4 turn 5 message reply re-sent re-sent re-sent re-sent N turns → ~N²/2 of the transcript re-sent
Every tool call is a turn, even in a bare Codex prompt.
Mathematics is reasoning.
The money is not.
Models are trained to be agentic. Give them tools, they call them.
Take the tools away, they reason.
2. Trust the model
get out of its way

The Bitter Lesson

Rich Sutton
“The biggest lesson that can be read from 70 years of AI research is that general methods that leverage computation are ultimately the most effective, and by a large margin.”
Hand-built structure competes with the model, removed structure compounds with it.

Why trust the model

judgmentyour code (cost: thousands) vs a reasoning model (cost: billions) informationthe reasoning is hidden
the model sees reasoning reply the harness sees hidden reply
today harness model environment tomorrow harness model environment
The model eats the harness, the harness eats the environment.

They build for the next model

Boris Cherny
“If you wait for the next model, and if you project out maybe three months, six months, most ideas will probably be good.”
Noam Brown
“The approach that we wanted to take was to just go toward the extreme end of baking in as little structure as we could and give the agents very primitive tools to use, and they figure out for themselves how to use them effectively.”

The Xean loop

task, notes, verdicts and the order: 1, 2, 3, repeat explore1 submits notes coordinator2 files, picks what to verify, guides the next turn verify3 verdicts ✓ a note passed every check the model the model the model the kernel
Harness enforces the workflow. Model makes all decisions. The notes are the whole environment.
Harness automatically captures model improvements
3. Verify independently
a separate call grades every note

Verification

lemma lemma a wrong gadget the result built on it verified accepted: every check passed, over verified support dead, because its support died
A dead note kills what stands on it.
4. Minimize cost
every token has a price

Verify once

✓lemma, checked once✓result 1✓result 2cites itcites it

A verified note is cited, never re-checked.

Verify the delta, and only what matters

draft, superseded✓the correction, a new notenever queuednotes are immutable. A fix is a new note.

Superseded notes are never verified.

No transcript

turn 1turn 2turn 3turn 4turn 5turn 6transcript, re-sent every turnXean: task, summaries, selected proofsinput per turn

Input per turn stays flat.

Each call sees as little as possible

explorethe task, every note’s summary, full text only for the support the coordinator picked verifythe notes under check and their support closure coordinatorevery note, as summaries and verdicts
Proofs travel once.
5. Survive interruptions
the notes are the only state

Durable by construction

explore coord verify explore coord killed here resume verify explore coord verify the journal … a person adds a note, any time
The mathematics is still there.
Ideas that looked good
and then did not

Ideas that looked good

Swarms Just retry, pass@k Forbid routes at the harness level Hill climbing on heuristics

Time is output

100k 1M 10M 1 h 2 h 4 h 8 h 16 h output tokens time one stream, about 140k tokens an hour Codex-goal ProofCouncil Rethlas QED Danus* Xean
The fast ones ran several streams in parallel.
*Danus at 12 h

Swarms

Noam Brown
“If you have four agents working on the problem, it is done twice as fast … you’re paying 2× more to get an answer twice as quickly.”
“I wouldn’t even attribute 10% of the credit to multi-agent.”
Swarms buy time with money.

Why fan-out does not scale

One run already tries a hundred approaches on its own.
1 2 3 4 5 6 7 8 9 10 ■ reasoning ■ the prefix each one re-reads one path led somewhere most paths end in a minute ten sub-agents, ten ways to attack the problem
Ten prefixes paid, one problem’s worth of thinking.

pass@k is the baseline

same prompt, k attempts, keep any success
zeroengineering freshevery attempt starts in a clean window k×the reasoning
At equal cost, nobody has shown an agent beating it.

Why dead notes should beat pass@k

Two routes. The model picks the wrong one 99 times in 100.
pass@k … ✓ about 100 attempts. Every attempt forgets. dead notes ✓ 2 attempts. The failed route is recorded, and not taken again.
Few branches, recorded failures: pruning wins.

What the context remembers

only failures prune the rootbreadth-first, by elimination only results ✓ ✓ ✓ anchor a pathdepth-first, on established results both ✓ ✓ ✓ Xeanrecorded, shown, never enforced
The model reads both and decides.
Xean, measured
what the run cost

Xean on 460 problems

190 solved, one GPT-6 Astra campaign per problem.
$9.96
per solved problem
$124 if every campaign is charged
65.7% reasoning
median$3.78, quartiles $2.30 and $7.95 verdicts5 failed, 1 inconclusive
Harness RAM: ≤200 MB per campaign, ≤92 GB for all 460 in parallel.
Xean archive

Solved problems are cheap

0 50 100 150 150 <$10 16 $10–20 11 $20–40 11 $40–80 2 $80–160 dollars spent per solved problem
Xean archive
Future ideas

Test a hypothesis

hypothesis without with hard problems, known solutions keep drop

Find the next hypothesis

route taken known proof guidance the step it missed, as a sentence

Hypotheses

Psychology. Do kind words help? Do harsh ones?
“You can do this.” ? “Wrong. Again.”
Proof search. Strategy, as guidance for the explorer.
guidance a sentence to the explorer, learned from the failures
The guidance will expire, the harness stays.

Open questions

Keep thinking. Ask it to go on, and reasoning per call decays.
problem reasoning “keep thinking” “keep thinking” “keep thinking” “keep thinking” “keep thinking” context
Balance. Exploration against verification.
✓lemma ✓lemma ✓the result nothing depends on it verify only what the result stands on