Erdős problem 21 - three n

It has been speculated (see e.g. [Ka94]) that the correct answer is

3n+O(1)

Withdrawn 5 Nov 2026

Withdrawn at the pool owner’s request after a report that Erdős 21 and 111 are solved. This withdrawal does not independently certify a proof of the exact selected target.

Formal statement

Proof target

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

namespace Bounty

theorem target : fcTypeOfName% "Erdos21.erdos_21.variants.three_n" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∃ C, ∀ᶠ (n : ℕ) in Filter.atTop, Erdos21.f n ≤ 3 * n + C ∧ 3 * n ≤ Erdos21.f n + C

Original conjecture source: FormalConjectures/ErdosProblems/21.lean

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

Task id: fc-v2-variants-three-n-1317e92b5821461f3bfe294f-formalized
Task commitment: sha256:ee27c1703190e0a41d38b5b9100087278895bd78c9b1782c8ca8bdc00da26780

References

erdosproblems.com/21

[Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.
[Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478.
[Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240.
[Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10.
[ErLo75] Erdős, P. and Lovász, L., *Problems and results on $3$ -chromatic hypergraphs and some related questions*. (1975), 609--627.
[Ka92b] Kahn, Jeff, On a problem of Erdős and Lovász: random lines in a projective plane. Combinatorica (1992), 417-423.
[Ka94] Kahn, Jeff, *On a problem of Erdős and Lovász. II. $n(r)=O(r)$ *. J. Amer. Math. Soc. (1994), 125-143.
[Tr14] A. Tripathi, A result on intersecting families with maximum transversal size. arXiv:1409.4610 (2014).
[BaWa21] J. Barát and I. M. Wanless, Intersecting and 2-intersecting hypergraphs with maximal covering number: the Erdős-Lovász theme revisited. J. Combin. Des. (2021), 260-286.

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

Combinatorics

Withdrawn

Date added 6 Nov 2026