72.lean`

2 declarations, 2 contain sorry, 0 declared as axioms

References:

erdosproblems.com/72
[Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.
[Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186.
[Er97b] Erdős, Paul, Some old and new problems in various branches of combinatorics. Discrete Math. (1997), 227-231.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[Bo77] Bollobás, Béla, Cycles modulo $k$. Bull. London Math. Soc. (1977), 97-98.
[Ve05] Verstraete, Jacques, Unavoidable cycle lengths in graphs. J. Graph Theory (2005), 151-167.
[LiMo20] Liu, Hong and Montgomery, Richard, A solution to Erdős and Hajnal's odd cycle problem. arXiv:2010.15802 (2020).

Imports (1)

theorem Erdos72.erdos_72 sorry line 67 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Set, Nat, And, Set.HasDensity, OfNat.ofNat, Real, Set.univ, Rat, LT.lt, Filter.Eventually, SimpleGraph, Fin, LE.le, SimpleGraph.averageDegree, Classical.propDecidable, SimpleGraph.Adj, SimpleGraph.Walk and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
23 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos72.erdos_72.variants.powers_of_two sorry line 80 source
depends on sorry what this means
Statement uses: Exists, Rat, And, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, SimpleGraph, Fin, LE.le, SimpleGraph.averageDegree, Classical.propDecidable, SimpleGraph.Adj, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.Walk.length, HPow.hPow, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.