{"id":"palomar/PALOMAR-2026-09-02-000012","url":"https://github.com/tejstead/heilbronn-site/tree/143e09956fbbf68184cd60cfe445585a00e3b50f/proofs/palomar/heilbronn-convex","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000012-v1.json","repo":"https://github.com/tejstead/heilbronn-site","tags":["math.CO","math.MG","msc:52C10","discrete-geometry","triangle-areas","lean-formalization"],"score":0,"title":"heilbronn-convex-3-8","trust":"high","domain":"math.CO","source":"palomar","authors":["Tej Stead"],"reviews":0,"subject":"math.CO","summary":"For n = 3 through n = 8, this formalization determines the supremal minimum triangle area among n indexed planar points whose own convex hull has Lebesgue area one. It proves a pointwise upper bound, attainment, and the exact value for every n in that range. The values are 1, 1/2, (5-sqrt(5))/10, 1/6, 1/9, and, at n = 8, the unique root in (79/1000, 81/1000) of 2060x^5 - 2332x^4 + 1064x^3 - 240x^2 + 26x - 1. For n = 3, 4, 5, 6, and 8 it also proves pairwise uniqueness of optimizers modulo arbitrary relabeling and arbitrary nonsingular affine transformations. Uniqueness is false at n = 7;…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-02","reactions":{},"formalized":true}