113.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/113
[ErSi84] Erdős, P. and Simonovits, M., Cube-supersaturated graphs and related problems. Progress in graph theory (Waterloo, Ont., 1982) (1984), 203-218.
[Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478.
[Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406.
[Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350.
[Ja23b] Janzer, Oliver, Disproof of a conjecture of Erdős and Simonovits on the Turán number of graphs with minimum degree 3. Int. Math. Res. Not. IMRN (2023), 8478--8494.

Imports (1)

theorem Erdos113.erdos_113 sorry line 59 source
depends on sorry what this means
Statement uses: Iff, False, Fintype, SimpleGraph, SimpleGraph.IsBipartite, Asymptotics.IsBigO, Nat, Real, Filter.atTop, SimpleGraph.extremalNumber, HPow.hPow, HDiv.hDiv, OfNat.ofNat, SimpleGraph.IsDegenerate
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.