Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify

• Single-session trajectories can propagate false claims, stall on missing knowledge, or appear successful after misunderstanding or weakening the task, with diminishing returns.Source: §1 · pp. 1–2
• HOA uses an artifact-centered worker–reviewer repair loop, routing structured wiki retrieval, independent semantic review, and task-specific verification as separate acceptance gates.A candidate is accepted only after all applicable gates pass; mathematical candidates are checked by a verifier without alteration.Source: §1 · p. 2
• HOA introduces a flow-level formalization that turns physics problems and figures into typed Lean statements and checks them against original problems for later agent-driven proof.Source: §1 · p. 3
• HOA reports full scores on IMO, IPhO, and IOI 2026, near-perfect IChO 2026, 672/672 PutnamBench solves, and #1 Lean-Eval with 251/304 (82.6%).Source: §1 · pp. 2–3
• The introduction reports that HOA boosts open-source models and can let open-weight models match or surpass standalone closed-source agents.Source: §1 · p. 3

2.1 LANGUAGE MODELS FOR FORMAL THEOREM PROVING

• Lean theorem proving includes specialized provers, tool-using agents, and proof-plan systems; HOA adds independent review, reusable knowledge, and task-specific verification beyond formal mathematics.Prior systems interleave reasoning with proof tokens or use reinforcement-learning-based proof search (Lin et al., 2025a; Google DeepMind, 2024).Source: §2.1 · p. 3

2.2 LONG-HORIZON RESEARCH AND OLYMPIAD AGENTS

• Prior agents add browsing and synthesis, hypothesis refinement (Gottweis et al., 2026), or verified, domain-specific olympiad workflows (Feng et al., 2026; Xu et al., 2025); HOA unifies these functions across four disciplines.Related work also includes evolutionary search and evaluations showing that both the base model and scaffold shape long-horizon performance (Novikov et al., 2025).Source: §2.2 · pp. 3–4

2.3 PROVER DRIVEN BY AGENT LOOPS

• AxiomProver generated Lean proofs for all 12 Putnam 2025 problems, while Aleph Prover plans subproblems, checks them in Lean, updates a global plan, and with GPT-5.2 reports solving 668 of 672 PutnamBench problems (Axiom, 2026; Isenbaev & Hanin, 2026).HOA separates generation, review, and verification: the reviewer provides evidence and specific revision requests, and the worker resubmits the revised artifact. For Lean tasks, Comparator builds the submission in a sandbox, matches it against the trusted statement, restricts permitted axioms, and checks the proof with the Lean kernel (Lean FRO, 2026).Source: §2.3 · p. 4
• HOA’s bounded, task-specific wiki differs from general retrieval systems by storing provenance-tracked accepted-proof lemmas for mathematics and drawing chemistry knowledge from multiple sources.Each run retrieves a small set of relevant records.Source: §2.3 · p. 4

3.1 OVERVIEW

• HOA combines a worker, independent reviewer, structured wiki, and task-specific verifier; candidates count as solved only after every required gate accepts them.The three feedback types are semantic evaluation, missing knowledge, and machine-evaluable testing, which the paper describes as complementary rather than interchangeable.Source: §3.1 · pp. 4–5

3.2 WORKER–REVIEWER LOOP

• An independent reviewer evaluates each frozen candidate against the original problem and acceptance criteria, returning unresolved findings to the worker for revision.The worker can consult the wiki and verifier, but must address reported issues and cannot accept its own output or bypass review.Source: §3.2 · p. 5

3.3 WIKIS FOR DOMAIN-SPECIFIC KNOWLEDGE

• Mathematics and chemistry use separate wikis: accepted Lean solutions yield reusable theorem records, while chemistry pages are curated before evaluation from textbooks, held-out olympiad problems, and references.Focused queries retrieve Lean declarations or chemistry concept pages; separate physics and coding wikis are omitted because the required knowledge is largely present in model pretraining.Source: §3.3 · p. 5

3.4 PHYSICS PROBLEM FORMALIZATION

• Physics problems are formalized as Lean theorems using Science Mango’s blueprint and LeanExplore searches over Mathlib and PhysLean before agents attempt proofs.A reviewer rejects statements with missing laws, omitted figure parameters, tautologies, or assumed answers; approved statements are frozen so the prover cannot weaken them. Sources: Science Mango, LeanExplore (Asher, 2025), Mathlib (mathlib Community, 2020), and PhysLean (Tooby-Smith, 2024).Source: §3.4 · pp. 5–6

3.5 VERIFIER

• For mathematics and formalized physics, Comparator checks Lean submissions against trusted challenge statements, restricts axioms, and validates exported proofs with the Lean kernel.The reviewer separately detects reward hacking or misunderstanding; for coding tasks, the worker and reviewer can run test cases and check correctness and time limits.Source: §3.5 · p. 6

4.1 EXPERIMENTAL SETUP

• The evaluation spans formalized IMO problems, PutnamBench, Lean-Eval, official IPhO, IChO, and IOI tasks, and a 50-problem Physics Cup subset, using task-appropriate proof or competition scoring.The study compares GPT-5.6 baselines from API call to agent with wiki and verifier to full HOA, plus open-weight models and public prover results where task sets and acceptance rules match.Source: §4.1 · pp. 6–7

4.2 MAIN RESULTS

• HOA reaches or exceeds 2026 gold thresholds on IMO, IPhO, IChO, and IOI, solves 672/672 PutnamBench problems, and solves 251/304 Lean-Eval problems (82.6%) versus GPT-5.6’s official 112/304 (36.8%).The Lean-Eval difference is 139 proofs and 45.7 percentage points; every formal proof is checked by the Lean kernel.Source: Table 1 · p. 7, §4.2 · p. 7

4.3 AN OPEN MODEL WITH AN OPEN HARNESS CAN MATCH CLOSED-SOURCE AGENTS

• With HOA, Kimi K3 achieves full marks on IOI, IMO, and IPhO and nearly matches GPT-5.6 on IChO, narrowing the open- versus closed-model gap compared with pure Codex.Table 2 compares HOA and pure Codex on the four 2026 competitions; Figure 3 shows convergence on PutnamBench.Source: §4.3 · p. 7, Table 2 · p. 8

4.4 ABLATION STUDY

• HOA performs best for every tested base model on both the 50-problem PutnamBench and Physics Cup evaluations, although the PutnamBench results are provisional.The comparisons span direct API calls, the original Codex harness, and full HOA, using GPT-5.6, Kimi K3, GLM-5.3, and DeepSeek V4 Pro.Source: §4.4 · p. 8, Table 3 · p. 8

4.5 ANALYSIS

• 63/100 versus 34/100: HOA reaches this Lean-Eval accuracy over 150 hours, while Pure Codex + /Goal plateaus after about 30 hours on the first 100 eligible problems.Failures remain in the denominator; the worker–reviewer loop converts sustained run time into verified solutions by recovering from intermediate failures.Source: §4.5 · pp. 8–9, Figure 4 · p. 9
• 47/50 versus 1/50 on PutnamBench for Kimi K3, and 50/50 versus 3/50 for GPT-5.6 Sol, are the full-HOA versus Codex /Goal results on the first 50 problems.The model gap narrows from 42 problems with Codex /Goal to 3 with the full Humanize loop.Source: Figure 3 · p. 9
• Three Comparator- and independently reviewed wiki records supplied Lean declarations for a G2 tensor-square theorem, whose final artifact passed Comparator and both the Nanoda and default Lean kernels.The records cover a 14-dimensional simple G2 quotient, a 64-dimensional irreducible highest-weight module, and fourteen irreducible tensor-square types; the agent used them directly rather than reproducing their proofs.Source: §4.5 · p. 9

5 CONCLUSION

• HOA uses a mandatory worker–reviewer repair loop, targeted wiki retrieval, and task-specific verification to detect errors, acquire knowledge, preserve specifications, and assess completion.Comparator checks mathematical candidates against trusted Lean statements, while programs retain their native execution tests.Source: §5 · p. 9
• HOA earns gold-medal-level performance across the 2026 IMO, IPhO, IChO, and IOI, full PutnamBench credit, and raises GPT-5.6 Lean-Eval solves from 112/304 to 251/304 (#1).An open-weight model with HOA also outperforms a closed-source standalone agent.Source: §5 · p. 10
• Future work will explore parallel workflows and divide-and-conquer strategies that split complex problems, solve parts independently, and combine the results.Source: §5 · p. 10

LIMITATIONS

• Finite benchmarks and constrained verification limit claims about HOA’s generalization and reliability, while possible contamination and unequal workflow resources weaken causal comparisons.Lean verification depends on faithful formalizations, and automated evaluators cover only encoded properties; experiments do not isolate every component interaction or fully characterize reviewer errors.Source: LIMITATIONS · p. 10

AI USE STATEMENT

• Generative AI assisted only with language polishing, grammar checking, and portions of the code; authors developed and take responsibility for the research and its final content.Authors reviewed AI-assisted text and verified and tested generated code for correctness.Source: AI USE STATEMENT · p. 10

ETHICS STATEMENT

• The work uses public benchmark and competition problems, involves no human subjects or personal data, and plans contamination audits; benchmark performance is not evidence of broad scientific autonomy.The authors will report uncertainty from auditing evaluation items for possible training contamination.Source: ETHICS STATEMENT · p. 10

REPRODUCIBILITY STATEMENT

• The HOA code supplement includes workflow implementation, runtime, benchmark inventory, prompts, orchestration, reviewer and verifier specifications, model and tool versions, budgets, logs, and Lean proof artifacts.Section 4 lists details of every benchmark and model checkpoint.Source: REPRODUCIBILITY STATEMENT · p. 10

Related work

• Formal-proving references include DeepSeek-Prover-V2, DeepSeek-Prover, DeepSeek-Prover-V1.5, TheoremLlama, Kimina-Prover Preview, and LongCat-Flash-Prover.Their titles describe reinforcement learning, synthetic data, proof-assistant feedback, Lean specialization, and agentic tool-integrated reasoning.Source: Z. Z. Ren, Zhihong Shao, Junxiao Song,… · pp. 13–14
• Agent-framework references include Reflexion, ReAct, A minimal agent for automated theorem proving, and work on scaling test-time compute for IOI gold.The listed titles describe verbal reinforcement learning, reasoning and acting, automated theorem proving, and test-time compute with open-weight models.Source: Z. Z. Ren, Zhihong Shao, Junxiao Song,… · pp. 14–15
• The bibliography also includes PutnamBench, LeanDojo, ChemLabs on Chemo, and HEPLearn, spanning theorem-prover evaluation, retrieval, chemistry, and high-energy physics.These topics are stated in the cited titles.Source: Z. Z. Ren, Zhihong Shao, Junxiao Song,… · pp. 14–15

A.1 EVALUATION INVENTORY

• The camera-ready inventory will report benchmark versions, competition years, release dates, maximum and HOA scores, verifier types, Lean artifact identifiers for mathematical problems, and contamination-audit status.The inventory is intended to make claims such as “perfect score” and “gold-medal-level” precise.Source: §A.1 · p. 15

A.2 REVIEWER RECORD TEMPLATE

• Reviewer records use an accept-or-revise verdict and findings with a location, error category, supporting evidence, and minimal requested repair.The schema begins with “verdict: accept | revise findings:” and defines the finding fields.Source: §A.2 · p. 15
• Accepted artifacts have no unresolved findings; disputed findings retain their evidence and final adjudication in the log.Source: §A.2 · p. 15

• The final appendix will report per-problem outcomes, confidence intervals, iteration curves, token and tool distributions, Comparator confusion analysis, wiki retrieval audits, and representative trajectories.Source: §A.3 · p. 15
• Case studies will include successful repairs, false reviewer alarms, false acceptances, and runs that exhaust their budgets to avoid selective reporting.Source: §A.3 · p. 15