63.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/63
[dBEr51] de Bruijn, N. G. and Erdős, P., A colour problem for infinite graphs and a problem in the theory of relations. Indag. Math. (1951), 369--373.
[ErHa66] Erdős, P. and Hajnal, A., On chromatic number of graphs and set-systems. Acta Math. Acad. Sci. Hungar. (1966), 61-99.
[LiMo20] Liu, Hong and Montgomery, Richard, A solution to Erdős and Hajnal's odd cycle problem. arXiv:2010.15802 (2020).
[Re24] Reiher, C., Graphs of large girth. arXiv:2403.13571 (2024).

Imports (1)

theorem Erdos63.erdos_63 sorry line 50 source
depends on sorry what this means
Statement uses: Iff, True, SimpleGraph, Eq, ENat, SimpleGraph.chromaticNumber, Top.top, Nat, Exists, And, GE.ge, Membership.mem, Set, SimpleGraph.cycleLengths, HPow.hPow, OfNat.ofNat
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.