A parallel prover built on HOA
We treat a long proof as a DAG of lemmas. A consumer posts each lemma as a GitHub issue as soon as every lemma it needs is proved, and producer agents running HOA flows claim the issues. Large lemmas are split into sub-issues (Decomposition · AND). When it is unclear whether splitting pays off, a lemma is proved directly and split at the same time (Speculation · OR). A hard lemma with several known proofs gets several agents on the same issue (Collaboration), and a search engine finds lemmas that already exist (search hit). A lemma closes only when Lean accepts it. The example is a simplified blueprint of the Poincaré conjecture by Perelman's route, Ricci flow with surgery.
Fifteen lemmas, from the Ricci flow equation down to the theorem. A lemma is dashed until everything it needs is proved, then it becomes an open issue, and it fills in when Lean accepts its proof. Pick a schedule to replay it, and click any lemma for details.
All hours are illustrative. They show how the techniques interact and are not measurements from our run. Wall clock is the time until the final theorem closes. Agent-hours add up the time every agent spent, including attempts that were stopped. The blueprint is a simplified outline of Perelman's argument; the formal proof has far more lemmas.
The theorem as a DAG of lemmas. A topological sort says which lemmas can start now.
Posts a lemma as a GitHub issue once every lemma it needs is closed.
Open issues wait for an agent, longest remaining chain first.
Agents claim issues and run an HOA flow: solve, review, wiki, verify. They may split an issue, prove it directly and split it at once, or share one issue.
The issue closes only when the Lean kernel accepts the proof.
↺ a closed issue unblocks the lemmas that need it, and the consumer posts them