Combinatorics

Date added 6 Nov 2026

Erdős problem 78

Let

R(k)

be the Ramsey number for

K_k

. Give a constructive proof that

R(k) > C^k

for some constant

C > 1

. Equivalently, give an explicit construction of graphs on

n

vertices which contain no clique and no independent set of size

\geq c \log n

, for some constant

c > 0

. We formalise "explicit" as: the adjacency relation of the graph on

n

vertices is decided by a single algorithm that runs in time polynomial in

n

(see explicitGraph). This is the weakest reasonable notion ("weakly explicit"); even this is open. The strongly explicit version, with time polynomial in

\log n

, is erdos_78.variants.strongly_explicit. This problem is #4 in Ramsey Theory in the graphs problem collection.

$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-erdos78-erdos-78-693f5ac83566626f2ebcf706-formalized →

Formal statement

Proof target

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

namespace Bounty

theorem target : fcTypeOfName% "Erdos78.erdos_78" := by
  sorry

end Bounty

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

Original conjecture (Lean type)

∃ c > 0,
  ∃ adj,
    ComplexityTheory.IsPolyTime adj ∧
      ∀ᶠ (n : ℕ) in Filter.atTop, Erdos78.NoHomogeneousSet (Erdos78.explicitGraph adj n) ⌈c * Real.log ↑n⌉₊

Original conjecture source: FormalConjectures/ErdosProblems/78.lean

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

Source type SHA-256: sha256:210da728798ca3809a9d18496ccc4a054375c16ce7ee677e3d01d57a97a5ad0e
Task id: fc-v2-erdos78-erdos-78-693f5ac83566626f2ebcf706-formalized
Task commitment: sha256:b6acc6465ff296793fb66ef7985f4eb17cef925f68758234be86f6863a1769c5

References

erdosproblems.com/78

[Co15] Cohen, Gil, Two-source dispersers for polylogarithmic entropy and improved Ramsey graphs. arXiv:1506.04428 (2015).
[Er47] Erdős, P., Some remarks on the theory of graphs. Bull. Amer. Math. Soc. (1947), 292-294.
Er71 Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.
[Er88] Erdős, P, Problems and results in combinatorial analysis and graph theory. Discrete Math. (1988), 81-92.
[Er93] Erdős, Paul, Some of my favorite solved and unsolved problems in graph theory. Quaestiones Math. (1993), 333-350.
[Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[Li23b] Li, Xin, Two source extractors for asymptotically optimal entropy, and (many) more. arXiv:2303.06802 (2023).
[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