FormalConjectures/ErdosProblems/1077.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 1077

Reference: erdosproblems.com/1077

Imports (1)
  1. theorem Erdos1077.erdos_1077 sorry line 43 source

    depends on sorry what this means

    Statement uses: Iff, False, Real, GT.gt, OfNat.ofNat, LT.lt, Filter.Eventually, Nat, SimpleGraph, Fin, Set.ncard, Sym2, SimpleGraph.edgeSet, HPow.hPow, HAdd.hAdd, Exists, SimpleGraph.Subgraph, And, SimpleGraph.IsBalanced, SimpleGraph.Subgraph.verts and 9 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.