Combinatorics

Date added 6 Nov 2026

Erdős problem 59 - big o

It is still possible (and conjectured by Morris and Saxton) that the weaker bound of

2^{O(\mathrm{ex}(n;G))}

holds for all

G

containing a cycle.

$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-variants-big-o-71839491b06091d590b74e12-formalized →

Formal statement

Proof target

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

namespace Bounty

theorem target : fcTypeOfName% "Erdos59.erdos_59.variants.big_o" := by
  sorry

end Bounty

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

Original conjecture (Lean type)

∀ (k : ℕ) (H : SimpleGraph (Fin k)),
  ¬H.IsAcyclic →
    ∃ C, 0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos59.numFree H n) ≤ 2 ^ (C * ↑(SimpleGraph.extremalNumber n H))

Original conjecture source: FormalConjectures/ErdosProblems/59.lean

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

Source type SHA-256: sha256:510c8d570c15b156c643d44d8cc07347244c0b8426d45266a0e4cd46c8129547
Task id: fc-v2-variants-big-o-71839491b06091d590b74e12-formalized
Task commitment: sha256:328892006c0a268ac70955fbf6aec65a775ea88eff346eedca96112918fd262c

References

erdosproblems.com/59

[EFR86] Erdős, P., Frankl, P. and Rödl, V., The asymptotic number of graphs not containing a fixed subgraph and a problem for hypergraphs having no exponent. Graphs Combin. (1986), 113-121.
[MoSa16] Morris, R. and Saxton, D., *The number of $C_{2\ell}$ -free graphs*. Adv. Math. (2016), 534-580. arXiv:1309.2927
[Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).

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