kim-emErdosUnitDistance

Formalization of Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture (companion to mathlib4 branch kim/erdos-unit-distance)
Displaying 1-1 of 1 packages depending on kim-em/ErdosUnitDistance
Sort by

  1. kim-em/ErdosUnitDistanceComparatorusescd25be5

    Independent comparator verification: the uniform-constant Erdős unit-distance conjecture is false (Alpöge 2026, formalized)