Primary evidence
- HyperTree Proof Search for Neural Theorem ProvingS1 · Primary research · Paper · 2022-05-23
- Evariste code accompanying HyperTree Proof SearchS1 · Primary research · Repository
HyperTree Proof Search introduces online self-improvement for neural theorem proving
The system learns from its own proof searches and uses a hyper-tree search algorithm inspired by Monte Carlo tree search and AlphaZero.
What happened?
HTPS plus online training reached 82.6% on held-out Metamath theorems and improved miniF2F-curriculum performance to 42%.
Why it matters
It foreshadowed the verifier-guided self-improvement loops that became common in later formal reasoning systems.
Significance rationale: HTPS coupled AlphaZero-inspired search with online learning and substantially advanced both Metamath and Lean theorem-proving performance.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Formal, Symbolic
- AI contribution
- The prover searches, learns from successful and failed search trajectories, and iteratively improves its policy.
- Human contribution
- Researchers designed HTPS, training environments and benchmark protocols.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- htps
- Organizations
- meta-ai
- Problems
- metamath, minif2f
- Methods
- online-training, tree-search, expert-iteration
Sources & artifacts
- HyperTree Proof Search for Neural Theorem ProvingS1 · Primary research · Paper · accessed 2026-09-10
- Evariste code accompanying HyperTree Proof SearchS1 · Primary research · Repository · accessed 2026-09-11
- Evariste HyperTree Proof Search research artifactArtifact · Code
Verification history
- 2022-05-23 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
Corrections
No corrections recorded.