Combinatorics

Date added 6 Nov 2026

Erdős problem 111

Erdős Problem 111 (Erdős, Hajnal, Szemerédi [EHS82]): If

G

is a graph with chromatic number

\aleph_1

, is it true that

h_G(n)/n \to \infty

? Formally: for every graph

G

(on a type

V

) with chromatic cardinal

\aleph_1

, the ratio

h_G(n)/n

tends to infinity: for every constant

C

, all sufficiently large

n

satisfy

h_G(n) > C \cdot n

$1,027 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-erdos111-erdos-111-89bf0a1f21464a8bb5556a05-formalized →

Formal statement

Proof target

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

namespace Bounty

theorem target : fcTypeOfName% "Erdos111.erdos_111" := by
  sorry

end Bounty

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

Original conjecture (Lean type)

∀ (V : Type) (G : SimpleGraph V),
  G.chromaticCardinal = Cardinal.aleph 1 → Filter.Tendsto (fun n => ↑(Erdos111.hG G n) / ↑n) Filter.atTop Filter.atTop

Original conjecture source: FormalConjectures/ErdosProblems/111.lean

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

Source type SHA-256: sha256:5c32b51c218ebe6b95623e5131e8c27b5dcbc626bc2bf7dce29f371ed3a113f5
Task id: fc-v2-erdos111-erdos-111-89bf0a1f21464a8bb5556a05-formalized
Task commitment: sha256:a7a03fc15511c81cd4e76be3e02d57d443143c760e953d435f3d94577accc268

References

erdosproblems.com/111

[Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. (1981)
[EHS82] Erdős, P., Hajnal, A., and Szemerédi, E., On almost bipartite large chromatic graphs. Theory and practice of combinatorics (1982), 117–123.
[Er87] Erdős, P., Some problems on finite and infinite graphs. (1987)
[Er90] Erdős, P., Some of my favourite unsolved problems. (1990)
[Er97d] Erdős, P., Some recent problems and results in graph theory. (1997)
[Er97f] Erdős, P., Some unsolved problems. (1997)

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