Erdős problem 60

Does every graph on

n

vertices with

>\mathrm{ex}(n;C_4)

edges contain

\gg n^{1/2}

many copies of

C_4

$1,024 bounty

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-erdos60-erdos-60-4854e6d26abf115821df40ff-formalized →

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«60»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos60.erdos_60" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

∃ c > 0,
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj],
      SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph 4) < G.edgeFinset.card →
        c * √↑n ≤ ↑{H' | Nonempty (H'.coe ≃g SimpleGraph.cycleGraph 4)}.ncard

Original conjecture source: FormalConjectures/ErdosProblems/60.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:ded82056dd6f01a0d5c30db65bd9ad87877ec9c2523187a02ec1cc2447d93748
Task id: fc-v2-erdos60-erdos-60-4854e6d26abf115821df40ff-formalized
Task commitment: sha256:d0b568a41908d0c067e6540dca2a7912c2b34c042fed77bfdd244615a0db4eac

References

erdosproblems.com/60

[HeMaYa21] He, J. and Ma, J. and Yang, T., Some extremal results on 4-cycles. Journal of Combinatorial Theory B (2021).

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord

∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj], SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph 4) < G.edgeFinset.card → c * √↑n ≤ ↑{H' | Nonempty (H'.coe ≃g SimpleGraph.cycleGraph 4)}.ncard