Erdos5480.1.0
Lean 4 Erdős problem #548 (Erdős–Sós conjecture): proof, found by GPT-6 Astra in the FrontierMath Erdős benchmark; Palomar submission repository
Sort by
Require Order
mathlib
v4.28.0The math library of Lean 4
Erdos5480.1.0v4.28.0