Erdős Problem a Daythe open tracker
The board / geometry / #507

Erdős Problem #507
Heilbronn's triangle problem

OPENdatabase updated 2025-08-31

No proof or disproof is known, and it isn't known whether a finite computation could settle it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

The minimum (unsigned) area of a triangle determined by three distinct points in a set `S`. Collinear triples count with area `0`. `EuclideanGeometry.triangle_area` is a signed area, so the absolute value is taken before the infimum.

\(\alpha(n)\) is the supremum of `minTriangleArea S` over all sets `S` of \(n\) points in the unit disk.

Current best lower bound [KPS82].

Let \(\alpha(n)\) be such that every set of \(n\) points in the unit disk contains three points which determine a triangle of area at most \(\alpha(n)\). Estimate \(\alpha(n)\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 6 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/507.
Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, Heilbronn: α(n) ≥ n^(−2+η), improving Komlós–Pintz–Szemerédi — family 191 at github.com/openai/math, a Lean file is linked. Bloom calls these claims, not endorsements; anything on this page that says the question is open was written before that release and has not re-checked it.
Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/507

Attempts

submit one →
WORKING REPORT BY THIS SITE · JUL 31, 2026

Read our working report →

Proved from scratch the exact radius-one-disk values α(3)=3√3/4, α(4)=1, and α(5)=√(5(5−√5)/32), plus the sharp all-boundary formula β(n)=2 sin²(π/n) sin(2π/n); the asymptotic Erdős problem remains op

PARTIAL
← #506the board#508 →