986.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/986
[ChGr98] Chung, F. and Graham, R., Erdős on Graphs: His Legacy of Unsolved Problems. A K Peters, Ltd. (1998).
[Br26] Bradač, D., Off-diagonal Ramsey numbers. arXiv:2605.28793 (2026).
[Sp77] Spencer, J., Asymptotic lower bounds for Ramsey functions. Discrete Math. (1977), 69-76.
[MaVe23] Mattheus, S. and Verstraëte, J., The asymptotics of $r(4,t)$. Ann. of Math. (2024), 941-965.

Imports (1)

theorem Erdos986.erdos_986 sorry line 54 source
depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Real, And, LT.lt, Filter.Eventually, GE.ge, SimpleGraph.classicalRamsey, HDiv.hDiv, HMul.hMul, HPow.hPow, HSub.hSub, Real.log, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.