Datasets › HOList
HOList
The official HOList benchmark for automated theorem proving consists of all theorem statements in the core, complex, and flyspeck corpora. The goal of the benchmark is to prove as many theorems as possible in the HOList environment in the order they appear in the database. That is, only theorems that occur before the current theorem are supposed to be used as premises (lemmata) in its proof.
Source: HoList Image Source: https://sites.google.com/view/holist/home
Benchmarks archive 2025-07-28
All 1 leaderboard whose dataset resolves to this page shown (sort by any header). "First row" is the archive's own first row at snapshot, in the archive's row order; nothing here re-ranks and metric direction is not asserted.
| First row (archive order) | Paper | Code | ||||
|---|---|---|---|---|---|---|
| Automated Theorem Proving | HOList benchmark | 4-hop GNN, sub-expression sharing Percentage correct 49.95 | Graph Representations for Higher-Order Logic and Theorem Proving | — | 4 | Compare |
Papers archive 2025-07-28
3 shown of 3 papers with a leaderboard row on this dataset's benchmarks, newest first. The archive's own "papers using this dataset" list was never published, so this is the benchmark-backed subset; the archive's count for this dataset is 8. The Syntology column is from Syntology's graph (read 2026-09-24), stated per sample; it is not part of any archive number.
| Date | Samples run Syntology | |||
|---|---|---|---|---|
| Learning to Reason in Large Theories without Imitation | 0 | 1 | 25 May 2019 | not harvested |
| Graph Representations for Higher-Order Logic and Theorem Proving | 0 | 1 | 24 May 2019 | not harvested |
| HOList: An Environment for Machine Learning of Higher-Order Theorem Proving | 3 | 2 | 5 Apr 2019 | not harvested |
Dataset loaders archive 2025-07-28
No loader listed in the archive.
Tasks archive 2025-07-28
License archive 2025-07-28
Unknown
Modalities archive 2025-07-28
Languages archive 2025-07-28
No language tagged.
Variants archive 2025-07-28
- HOList benchmark
- HOList
2 variant names, as the archive lists them.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections