Convex, n = 5 proven

A =

\frac{5 - \sqrt{5}}{10}

= 0.276393202250021030359082633126872376455938164…

root of

5 x^{2} - 5 x + 1

— regular pentagon: three consecutive vertices span 4 sin²36° / 5 of its area

5 minimal triangles in 1 congruence classes, colored by class.

Symmetry

5-fold dihedral symmetry (group D5, order 10).

5 points in 1 orbit (5) — hover a point to see its orbit.

5 triangles tied (within relative 10⁻⁹) at the minimal area:

	count	side lengths	triangles (point indices)
	5	`1.1756 · 1.1756 · 1.9021`	(0,1,2) (0,1,4) (0,3,4) (1,2,3) (2,3,4)

Found by David Cantrell, June 2007.
Proved optimal by Tej Stead, August 2026.
The optimality proof is machine-checked in Lean 4: value, attainment, and uniqueness of the affinely regular pentagon up to relabeling and invertible affine maps. Registered in the Palomar registry (PALOMAR-2026-09-02-000012).
Coordinates generated from the exact construction: data/sources/exact/constructions.py — regular pentagon.
Verified in exact arithmetic: all 10 triples enumerated, 5 tied at the minimum.

2026-08-22 marked proven: optimality of the regular pentagon proved by Tej Stead, August 2026 (unpublished; link to follow)
2026-09-02 proof link added: the August 2026 optimality proof is now machine-checked in Lean 4 and public in the site repository (proofs/palomar/heilbronn-convex)
2026-09-03 proof registered: Palomar registry entry PALOMAR-2026-09-02-000012 v1