163.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/163
[BuEr75] Burr, S. A. and Erdős, P., On the Ramsey number of graphs with small degree-ratio. Colloq. Math. Soc. János Bolyai (1975).
[Le17] Lee, C., Ramsey numbers of degenerate graphs. Ann. of Math. (2) 185 (2017), 791-829.

Imports (1)

theorem Erdos163.erdos_163 sorry line 49 source
depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Exists, Real, And, GT.gt, Fintype, SimpleGraph, SimpleGraph.IsDegenerate, SimpleGraph.diagonalGraphRamsey, HMul.hMul, Fintype.card
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.