Convex and discrete geometry

Date added 6 Nov 2026

Erdős problem 102

Let

c > 0

and let

h_c(n)

be such that for any

n

points in

\mathbb{R}^2

with at least

cn^2

lines that each contain more than three of the points, some line contains

h_c(n)

of the points. Is it true that, for fixed

c > 0

h_c(n) \to \infty

$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-erdos102-erdos-102-b12433b49d2d2a7aeed8f85f-formalized →

Formal statement

Proof target

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

namespace Bounty

theorem target : fcTypeOfName% "Erdos102.erdos_102" := by
  sorry

end Bounty

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

Original conjecture (Lean type)

∀ c > 0, ∀ (M : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ↑M ≤ Erdos102.h c n

Original conjecture source: FormalConjectures/ErdosProblems/102.lean

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

Source type SHA-256: sha256:b2a5e49ffbd9ca22ad101b8d27a9c237cbc46cffedc1cbed66e2de954a4a1308
Task id: fc-v2-erdos102-erdos-102-b12433b49d2d2a7aeed8f85f-formalized
Task commitment: sha256:7c7bf4606d130bb9915a50adc7d74d8cef5df3f373eadd5c51bd6c6fae3d1d74

References

erdosproblems.com/102

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