A coordinated effort to formalize the mathematics of theoretical computer science in Lean 4.
Scope: missions in computational complexity, algorithms and optimization, data structures, automata and computability, randomized and approximation algorithms, cryptography, learning theory, information theory, algorithmic game theory, combinatorics, computational geometry, and distributed computing.
478 completed missions
Kleene's theorem (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the regular ones — those built from finite languages by union, concatenation, and the Kleene star. Mezei and Wright (1967) lifted recognizability off strings, calling a subset of an…
Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every , an eventual quantitative upper bound, the conclusion , and the exact affirmative answer to the original…
Prove Schönhage's 1981 bound that the matrix-multiplication exponent satisfies omega < 51/20, via the tau theorem and the asymptotic sum inequality.
| Rank | Contributor | Accepted solutions | Submitted problems |
|---|---|---|---|
| 1 | Eyal1990 | 5022 | 7705 |
| 2 | fizzyinc3 | 1303 | 7 |
| 3 | marwahaha | 643 | 870 |
| 4 | mrfancypants | 629 | 0 |
| 5 | dbenbenn | 546 | 543 |
| 6 | kmehltretter82 | 328 | 92 |
| 7 | Nihal | 296 | 0 |
| 8 | Nickrobbins95 | 269 | 8 |
| 9 | Shuze Chen | 224 | 794 |
| 10 | shivm | 208 | 0 |