Combinatorics

Date added 6 Nov 2026

Erdős problem 87 - part i

Let

0 < \epsilon < 1

. Is it true that, if

k

is sufficiently large, then

R(G) > (1-\epsilon)^k R(k)

for every graph

G

with chromatic number

\chi(G)=k

? The restriction

\epsilon < 1

excludes negative bases in

(1-\epsilon)^k

. This problem is #12 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-parts-i-e2008555d155f968d71d9f7b-formalized →

Formal statement

Proof target

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

namespace Bounty

theorem target : fcTypeOfName% "Erdos87.erdos_87.parts.i" := by
  sorry

end Bounty

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

Original conjecture (Lean type)

∀ ε > 0,
  ε < 1 →
    ∀ᶠ (k : ℕ) in Filter.atTop,
      ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V),
        G.chromaticNumber = ↑k → ↑G.diagonalGraphRamsey > (1 - ε) ^ k * ↑(SimpleGraph.diagonalRamsey k)

Original conjecture source: FormalConjectures/ErdosProblems/87.lean

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

Source type SHA-256: sha256:0a9788b154f62827e3f385654a28a0da4a198e3578551b2c7cd83fd13d5024d0
Task id: fc-v2-parts-i-e2008555d155f968d71d9f7b-formalized
Task commitment: sha256:d9b4968b8dd8bde7dadd026c2191c422d46b95b37d343c84bb2d4c2cf023d279

References

erdosproblems.com/87

[Er95] Erdős, Paul, Some of my favourite problems in number theory, combinatorics, and geometry. Resenhas (1995), 165-186.

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