In August this flow took first place on the Lean-Eval leaderboard. That board no longer exists in the same shape. The maintainers have frozen a first release, LeanEval v1, of 128 problems (published 20 August 2026), and moved the older problems to an Archive of 171. The leaderboard now shows one scope at a time, and a single "first place" no longer describes it. Here is where we stand in each.
All numbers below come from the board's own published data, generated 2026-10-05 08:56 UTC. Our entry is listed as "Humanifa + GPT 5.6 sol" (sic).
LeanEval v1: 128 problems, 88 solved by anyone
| Entry | Unique | First solves | Total |
|---|---|---|---|
| Axiom Prover (Axiom Math) | 3 | 21 | 74 |
| NEAR AI, with DeepSeek V4 | 3 | 12 | 80 |
| Humanfia, GPT-5.6 | 1 | 30 | 79 |
- First solves: first, with 30. We were the first to have an accepted proof on 30 of the 88 problems anybody has solved.
- Total: second, with 79, one behind NEAR AI's 80.
- Unique: fourth. Only one of our 79 has no other solver. The board sorts by this column by default, so that is the position a visitor sees first.
The three columns reward different things: being first, being alone, or being broad. We lead on the first and are close on the third. Others have more problems nobody else can do.
Archive: 170 of 171
On the 171 archived problems we have accepted proofs for 170, tied for the most with two other entries. Counted across both scopes, 249 distinct problems carry an accepted Humanfia proof, the most of any entry on the board. That count is ours, made from the published data; the site does not show a combined column. The board also notes that one model may appear under more than one name while names are consolidated.
What counts
Lean-Eval accepts a solution only when it passes Comparator against the problem's statement. There are no partial credits and no sorry. Of the entry's 249 accepted solutions, 210 were submitted by Zhengyang Zhang, 34 by Hongzhou Lin and 5 by Jui-Hui Chung; 75 were accepted on or after 19 August.