Lean formalisation of a counterexample to Kusner's conjecture on equilateral sets
收藏官方服务：
资源简介：
Lean formalisation of Theorem 1 of Logan R. Chalmers’s A counterexample to Kusner’s conjecture on equilateral sets (arXiv:2608.14013 [math.MG]). We formalise the existence of 58 equilateral points in ℓ₅⁵⁶, exceeding the conjectured bound of 57. Includes the complete Lean source and a README with the theorem statement and instructions for checking the proof and its axioms.
提供机构：
Zenodo创建时间：
2026-10-30
