Track 2 Leaderboard

TCS Proving in Lean. Combined Phase 1 + Phase 2 ranking out of 1000 points. See Scoring Rules for the full per problem scoring criteria and the tie-break cascade.

All times on this page are UTC. We sweep Codabench for new submissions roughly every 48 hours and score each new batch shortly after.
Last updated: 2026-06-22 16:42 Last collection: 2026-06-16 14:21 Verifier: SafeVerify Submissions scored: 182
Per problem leaderboard
Rank Submitter Solved Score % Total Score Splay constant Heartbeats Bytes Submission Time ID
🥇1 cmxu7(13 attempts) 31 / 34 65.0% 650 / 1000 D — · S 7.5 590,261 508,986 2026-06-16 11:36 799861
🥈2 lmilikic(7 attempts) 31 / 34 65.0% 650 / 1000 D — · S 8 1,155,407 562,193 2026-06-16 13:55 800029
🥉3 janko_cameron_lean4-skills(16 attempts) 31 / 34 65.0% 650 / 1000 D — · S 8.33 423,995 409,496 2026-06-16 01:22 799265
4 jason_bourne(4 attempts) 31 / 34 65.0% 650 / 1000 D — · S 18 1,411,085 271,598 2026-06-15 16:31 798793
5 allenzhu(21 attempts) 31 / 34 65.0% 650 / 1000 D — · S 21 399,644 296,010 2026-06-14 04:44 795857
6 paws08(3 attempts) 31 / 34 65.0% 650 / 1000 D — · S 52 563,838 360,358 2026-06-15 18:56 799029
7 minjaeso(3 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 138,659 21,823 2026-06-15 19:02 799044
8 jasperdekoninck(8 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 234,235 305,989 2026-06-15 17:08 798862
9 ctree4113(8 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 325,150 241,509 2026-06-13 11:30 794724
10 bhwang(9 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 333,858 300,774 2026-06-15 15:03 798657
11 lcthej(4 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 618,425 410,591 2026-06-12 11:43 793246
12 ygdjiang(4 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 895,305 279,832 2026-06-14 15:26 796843
13 zerol(3 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 907,500 370,898 2026-06-13 06:44 794352
14 fabianz(2 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 952,332 305,229 2026-06-14 20:34 797405
15 nielstron 30 / 34 60.0% 600 / 1000 D — · S — 967,370 362,059 2026-05-28 18:01 763078
16 chensun 30 / 34 60.0% 600 / 1000 D — · S — 967,370 362,059 2026-05-29 15:53 765555
17 hypergalois(2 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 1,045,637 296,718 2026-06-08 00:43 784932
18 atrin(3 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 1,092,890 258,431 2026-06-02 05:21 775010
19 dmytruto(3 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 1,163,356 458,454 2026-06-10 11:07 789486
20 maudlemercier(2 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 1,420,381 939,225 2026-06-03 12:17 777554
21 squak(2 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 6,133,679 282,344 2026-06-16 00:00 799221
22 aurasoph(5 attempts) 30 / 34 60.0% 600 / 1000 D — · S — 6,671,890 298,262 2026-06-15 08:06 798121
23 daniil_shmelev(3 attempts) 29 / 34 57.5% 575 / 1000 D — · S — 2,055,675 337,848 2026-06-13 21:38 795622
24 codyx(3 attempts) 29 / 34 52.0% 520 / 1000 D — · S — 736,225 237,165 2026-06-08 18:09 786623
25 robertboy18(2 attempts) 29 / 34 50.0% 500 / 1000 D — · S — 822,596 262,701 2026-05-20 22:29 743754
26 sunny99(7 attempts) 29 / 34 50.0% 500 / 1000 D — · S — 869,102 288,822 2026-05-21 12:47 745249
27 jszhang 29 / 34 50.0% 500 / 1000 D — · S — 942,144 287,126 2026-05-19 08:48 740372
28 marcusm117(2 attempts) 29 / 34 50.0% 500 / 1000 D — · S — 992,172 447,944 2026-05-09 23:00 719913
29 sandeepsaluru(2 attempts) 29 / 34 50.0% 500 / 1000 D — · S — 1,907,006 402,173 2026-05-25 18:38 755093
30 maximiliano(4 attempts) 29 / 34 50.0% 500 / 1000 D — · S — 2,464,097 178,808 2026-05-17 15:28 736267
31 xvade(2 attempts) 29 / 34 50.0% 500 / 1000 D — · S — 5,944,287 258,717 2026-05-18 20:37 739590
32 xuanfeiren(4 attempts) 28 / 34 40.0% 400 / 1000 D — · S — 898,103 159,101 2026-05-16 01:26 733498
33 allenanie 28 / 34 40.0% 400 / 1000 D — · S — 1,455,897 369,770 2026-05-19 04:20 739971
34 sumukhmg(2 attempts) 27 / 34 32.0% 320 / 1000 D — · S — 659,062 121,465 2026-06-12 05:57 792756
35 guojing0 27 / 34 32.0% 320 / 1000 D — · S — 1,007,873 133,007 2026-05-19 11:29 740669
36 auraq 23 / 34 27.2% 272 / 1000 D — · S — 567,430 133,787 2026-05-17 21:11 736752
37 shuwesley(2 attempts) 17 / 34 21.6% 216 / 1000 D — · S — 434,794 79,004 2026-05-30 06:27 767094
38 snowpine007 3 / 34 16.0% 160 / 1000 D — · S — 87,088 81,294 2026-05-22 06:27 747085
39 jjyyy(2 attempts) 3 / 34 16.0% 160 / 1000 D — · S — 167,816 63,207 2026-05-07 22:24 716101
40 msantolu 19 / 34 16.0% 160 / 1000 D — · S — 332,576 68,018 2026-05-18 21:04 739618
41 jxb222 19 / 34 16.0% 160 / 1000 D — · S — 399,390 62,324 2026-05-09 10:01 718997
42 yhn112(9 attempts) 2 / 34 4.4% 44 / 1000 D — · S — 27,508 3,216 2026-05-10 20:50 721519
43 kpal002(2 attempts) 2 / 34 1.4% 14 / 1000 D — · S — 25,274 3,318 2026-06-06 09:34 782504
44 thomsdenoms(2 attempts) 3 / 34 1.2% 12 / 1000 D — · S — 19,131 2,028 2026-06-16 00:30 799228
45 kurone02 0 / 34 0.0% 0 / 1000 D — · S — 0 0 2026-05-08 16:32 717745
46 manishacharya 0 / 34 0.0% 0 / 1000 D — · S — 0 0 2026-05-26 02:50 755525
47 brendanlo 0 / 34 0.0% 0 / 1000 D — · S — 0 — 2026-05-26 15:00 756984
📋 Scoring Rules Open Track 2 challenge page
Submissions are scored against the reference Lean project using lake build, an axiom whitelist (propext, Quot.sound, Classical.choice), and a signature match against the reference theorem. Files containing sorry score zero on the corresponding problem. Ties on total score are broken by the cascade documented on the Scoring Rules page: the smaller Splay Tree constant on the Deque problem, then the smaller constant on the Sequential problem, then proof heartbeats, then proof bytes (comments stripped), then submission time.