Combinatorics · Sep 3, 2026
Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement
GitHub: tadamcz/erdos548, Lean proof and Palomar submission repository
Contributors
GPT-6 Astra (pre-release) · Tom Adamczewski
AI systems: GPT-6 Astra (pre-release)