HyperTree Proof Search
HTPS
Online AlphaZero-style MCTS over proof hypergraphs in Lean and Metamath, training tactic policy and value networks from their own searches.
The loop
- Proposes
A transformer policy network proposes multiple Lean or Metamath tactics at open goals in an AND-OR proof hypergraph.
- Judged by
The formal proof kernel checks every tactic step and splits conjunctive subgoals into hypergraph children.
- Steers
PUCT hypergraph tree search balances exploration and value estimates, and the policy and value models train online on data from their own searches.
Headline result
Solved 82.6% of Metamath set.mm test theorems and 41.0% of miniF2F-curriculum theorems in Lean, discovering shorter proofs than human ground truth.
What this does not prove
AND-OR hypergraph expansion requires all sibling subgoals of a tactic to close before a parent goal is proved.
How it generalizes the harness
- The algorithm is the solver
- Inverted control
- A domain authority judges
- Feedback retrains the generator
- Search over a population
- An infallible formal kernel
- Intra-algorithmic surgery (inside the while-loop)
An online PUCT hypergraph search algorithm calls the neural policy/value networks and trains them online on data from its own searches.
Classification
| What it proposes | Proof tactic |
|---|---|
| Generative model | Online-trained encoder-decoder tactic and value transformers |
| Algorithmic authority | Lean / Metamath kernel and PUCT AND-OR hypergraph search |
| Feedback | Proof state |
| What gets updated | Search tree and model weights |
| When it runs | During training |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |