Per challenge breakdown for submission 777554 on 2026-06-03 12:17.
Verifier: SafeVerify. Last updated 2026-06-22 16:42.
| File | Theorem | Status | Score |
|---|---|---|---|
| Phase 1 | |||
| Binary Heap and Dijkstra | |||
| Challenge_BinaryHeap_1.lean141 | heapify_correctness | PASS | 25 / 25 |
| Challenge_BinaryHeap_2.lean132 | extract_min_correctness | PASS | 25 / 25 |
| Challenge_BinaryHeap_3.lean142 | insert_correctness | PASS | 25 / 25 |
| Challenge_BinaryHeap_4.lean136 | decrease_priority_correctness | PASS | 25 / 25 |
| Challenge_Dijkstra_1.lean145 | extract_min_is_someHeap | PASS | 10 / 10 |
| Challenge_Dijkstra_2.lean139 | dijkstra_terminate | PASS | 10 / 10 |
| Challenge_Dijkstra_3.lean117 | dijkstra_correctness | PASS | 80 / 80 |
| Minimum Spanning Tree | |||
| Challenge_Kruskal.lean104 | kruskal_computes_MST | PASS | 100 / 100 |
| Segment Tree | |||
| Challenge_CoverageIntervalDefs.lean132 | coverage_interval | PASS | 20 / 20 |
| Challenge_Build.lean156 | build | PASS | 40 / 40 |
| Challenge_Query_1.lean137 | query_correctness | PASS | 20 / 20 |
| Challenge_Query_2.lean136 | query_time | PASS | 20 / 20 |
| Treap analysis (probabilistic) | |||
| Challenge_Analysis_1.lean137 | prob_is_ancestor | PASS | 10 / 10 |
| Challenge_Analysis_2.lean132 | expected_depth | PASS | 30 / 30 |
| Treap algorithms | |||
| Challenge_Treap_1.lean150 | all_keys_union_merge | PASS | 4 / 4 |
| Challenge_Treap_2.lean140 | split_properties | PASS | 4 / 4 |
| Challenge_Treap_3.lean141 | split_correct | PASS | 4 / 4 |
| Challenge_Treap_4.lean141 | splitUpper_correct | PASS | 4 / 4 |
| Challenge_Treap_5.lean142 | merge_IsBST | PASS | 4 / 4 |
| Challenge_Treap_6.lean142 | merge_IsHeap | PASS | 4 / 4 |
| Challenge_Treap_7.lean137 | insert_inserts_element | PASS | 4 / 4 |
| Challenge_Treap_8.lean137 | delete_deletes_element | PASS | 4 / 4 |
| Challenge_Treap_9.lean137 | find_finds_element | PASS | 4 / 4 |
| Challenge_Treap_10.lean146 | splitT_correctness | PASS | 4 / 4 |
| Challenge_Treap_11.lean143 | splitT_time | PASS | 4 / 4 |
| Challenge_Treap_12.lean144 | splitUpperT_correctness | PASS | 4 / 4 |
| Challenge_Treap_13.lean144 | splitUpperT_time | PASS | 4 / 4 |
| Challenge_Treap_14.lean144 | mergeT_correctness | PASS | 4 / 4 |
| Challenge_Treap_15.lean144 | mergeT_time | PASS | 4 / 4 |
| Phase 1 subtotal | 500 / 500 | ||
| Phase 2 | |||
| Splay Tree | |||
| Challenge_Splay_Sequential.lean35 | sequential | MISSING | 0 / 50 |
| Challenge_Splay_Deque.lean0 | deque | MISSING | 0 / 50 |
| Challenge_Splay_DequeConjecture.lean0 | deque_conjecture | MISSING | 0 / 100 |
| Challenge_Splay_TraversalConjecture.lean0 | traversal_conjecture | MISSING | 0 / 200 |
| Spanner | |||
| Challenge_Spanner.lean88 | spanner_exists | PASS | 100 / 100 |
| Phase 2 subtotal | 100 / 500 | ||
| Total | 600 / 1000 | ||
Each blue dot is one problem this submission solved. X axis is how long the proof source is in bytes (comments stripped). Y axis is how much elaboration work it took Lean, measured in heartbeats (a deterministic CPU-style counter; lower is more efficient). Both axes are log scale. Larger dots are worth more points. Hover any dot to see the problem name. Dots in the lower left are short and fast proofs; dots in the upper right are the heavy ones.
All 182 submissions by time × score. Hover for submitter, click to open.
this same submitter others
lake build against the reference project and the named theorem must use only the permitted axioms propext, Quot.sound, Classical.choice. Files containing sorry score zero on the corresponding problem.