Per challenge breakdown for submission 721529 on 2026-05-10 21:06.
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 | MISSING | 0 / 25 |
| Challenge_BinaryHeap_2.lean132 | extract_min_correctness | MISSING | 0 / 25 |
| Challenge_BinaryHeap_3.lean142 | insert_correctness | MISSING | 0 / 25 |
| Challenge_BinaryHeap_4.lean136 | decrease_priority_correctness | MISSING | 0 / 25 |
| Challenge_Dijkstra_1.lean145 | extract_min_is_someHeap | MISSING | 0 / 10 |
| Challenge_Dijkstra_2.lean139 | dijkstra_terminate | MISSING | 0 / 10 |
| Challenge_Dijkstra_3.lean117 | dijkstra_correctness | MISSING | 0 / 80 |
| Minimum Spanning Tree | |||
| Challenge_Kruskal.lean104 | kruskal_computes_MST | FAIL | 0 / 100 |
| Segment Tree | |||
| Challenge_CoverageIntervalDefs.lean132 | coverage_interval | FAIL | 0 / 20 |
| Challenge_Build.lean156 | build | PASS | 40 / 40 |
| Challenge_Query_1.lean137 | query_correctness | MISSING | 0 / 20 |
| Challenge_Query_2.lean136 | query_time | MISSING | 0 / 20 |
| Treap analysis (probabilistic) | |||
| Challenge_Analysis_1.lean137 | prob_is_ancestor | MISSING | 0 / 10 |
| Challenge_Analysis_2.lean132 | expected_depth | MISSING | 0 / 30 |
| Treap algorithms | |||
| Challenge_Treap_1.lean150 | all_keys_union_merge | MISSING | 0 / 4 |
| Challenge_Treap_2.lean140 | split_properties | MISSING | 0 / 4 |
| Challenge_Treap_3.lean141 | split_correct | MISSING | 0 / 4 |
| Challenge_Treap_4.lean141 | splitUpper_correct | MISSING | 0 / 4 |
| Challenge_Treap_5.lean142 | merge_IsBST | MISSING | 0 / 4 |
| Challenge_Treap_6.lean142 | merge_IsHeap | MISSING | 0 / 4 |
| Challenge_Treap_7.lean137 | insert_inserts_element | MISSING | 0 / 4 |
| Challenge_Treap_8.lean137 | delete_deletes_element | MISSING | 0 / 4 |
| Challenge_Treap_9.lean137 | find_finds_element | MISSING | 0 / 4 |
| Challenge_Treap_10.lean146 | splitT_correctness | MISSING | 0 / 4 |
| Challenge_Treap_11.lean143 | splitT_time | MISSING | 0 / 4 |
| Challenge_Treap_12.lean144 | splitUpperT_correctness | MISSING | 0 / 4 |
| Challenge_Treap_13.lean144 | splitUpperT_time | MISSING | 0 / 4 |
| Challenge_Treap_14.lean144 | mergeT_correctness | MISSING | 0 / 4 |
| Challenge_Treap_15.lean144 | mergeT_time | MISSING | 0 / 4 |
| Phase 1 subtotal | 40 / 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 | MISSING | 0 / 100 |
| Phase 2 subtotal | 0 / 500 | ||
| Total | 40 / 1000 | ||
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.