705.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/705
[OD99] P. O'Donnell, High girth unit-distance graphs. PhD Dissertation, Rutgers University (1999).

Imports (1)

theorem Erdos705.erdos_705 sorry line 44 source
depends on sorry what this means
Statement uses: Iff, False, Exists, Nat, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Set.Finite, GE.ge, SimpleGraph.girth, SimpleGraph.UnitDistancePlaneGraph, LE.le, ENat, SimpleGraph.chromaticNumber
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.