Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify
On the map: LLM agents and tool use → Educational agents and math problem solving
Abstract (arXiv)
Large language model (LLM) agents are rapidly improving on long-horizon scientific and olympiad tasks. Recent systems have produced a Lean-formalized resolution of the Navier--Stokes problem and autonomous solutions to four open questions in the ErdHos Conjectures database. Yet neither system releases both its underlying model and complete inference stack. More broadly, a single agent session remains brittle on difficult problems: early errors can propagate, missing domain knowledge can stall progress, and apparent success can mask a misinterpretation or weakening of the original task. We introduce HOA (Humanize Olympiads Agent), an open, flow-level framework that coordinates multiple agent sessions through three complementary feedback channels. First, an independent reviewer evaluates each candidate and provides actionable feedback. Second, a structured wiki supplies task-specific knowledge that may be missing or unreliable in model pretraining. Third, a verifier checks generated Lean proofs against trusted challenge statements. With GPT-5.6 Sol, HOA achieves perfect scores on the IMO, IPhO, and IOI 2026, near-full marks on the IChO 2026 problem set, and solves all 672 problems (100%) on PutnamBench. On the Lean-Eval leaderboard, HOA ranks first, solving 251 of 304 problems (82.6%). We further evaluate HOA with open models. Using Kimi-K3, HOA achieves full scores on the IMO, IPhO, and IOI, and a gold-level score of 97.1% on the IChO. These results closely match the closed-source GPT-5.6 Sol + /Goal baseline on the IMO and IPhO, while exceeding it on the IChO and IOI, demonstrating that systematic feedback can help bridge substantial differences in base-model capability.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. Builds on 29 of its 51 references that are in the map. First posted on arXiv 9 Oct 2026.
Builds on
29 of 51 references.
Closest ancestors · 6
Same direction, newest first
- 2026Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement4 Jun
- 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks2 Jun
- 2026OProver: A Unified Framework for Agentic Formal Theorem Proving17 May
- 2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent29 Apr
- 2026A Minimal Agent for Automated Theorem Proving27 Feb
- 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics20 Jan
Other references · 23
- 2020Retrieval-Augmented Generation for Knowledge-Intensive NLP Taskscited by 9,297
- 2023Reflexion: Language Agents with Verbal Reinforcement Learningcited by 4,276
- 2024The AI Scientist: Towards Fully Automated Open-Ended Scientific Discoverycited by 1,071
- 2023Large Language Models Cannot Self-Correct Reasoning Yetcited by 1,017
- 2025AlphaEvolve: A coding agent for scientific and algorithmic discoverycited by 867
- 2023CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquingcited by 783
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
- 2025Accelerating scientific discovery with Co-Scientistcited by 401
- 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
- 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
- 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
- 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
11 more
- 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
- 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
- 2025Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipelinecited by 82
- 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 59
- 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 33
- 2025LeanExplore: A search engine for Lean 4 declarationscited by 18
- 2025Scaling Test-Time Compute to Achieve IOI Gold Medal with Open-Weight Modelscited by 10
- 2026LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learningcited by 7
- 2025ChemLabs on ChemO: A Multi-Agent System for Multimodal Reasoning on IChO 2025cited by 3
- 2026VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Provingcited by 2
- 2026Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditingcited by 1
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2024Can Language Models Solve Olympiad Programming?
- 2025Xolver: Multi-Agent Reasoning with Holistic Experience Learning Just Like an Olympiad Team
- 2026RMA: an Agentic System for Research-Level Mathematical Problems
- 2026Harnessing the Collective Intelligence of AI Agents in the Wild for New Discoveries
- 2026ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
- 2025PhysicsMinions: Winning Gold Medals in the Latest Physics Olympiads with a Coevolutionary Multimodal Multi-Agent System
- 2025Diverse Inference and Verification for Advanced Reasoning
- 2026An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics