GitHub radar
Open AI Ten Proofs in Lean 4
Ten contributions in theoretical computer science and math, such as sphere packing, quantum games, Erhart volume, and others, verified by machine checkable formal proofs in Lean 4.
Ten new theorems in mathematics and theoretical computer science proved with fully machine-checked Lean 4 proofs. Binary codes, spherical codes, non-sofic groups, Connes’s Rigidity Conjecture, quantum game repetition, closet vector problem, Erhart volume conjecture, multicolored Ramsey numbers, extremal combinatorics.
Why a vibe-coder should care
AI is beginning to help solve problems in parts of math that had resisted solution for decades. We also get a quantitative measure of AI’s advances in logical thinking by seeing that the proofs are completely transparent to machines.
▌ More finds