Maximum-area small polygons (largest small polygon problem)

### What is the conjecture

I would like to add the classical largest small polygon problem.

For each integer $n\geq 3$, let $\mathcal P_n$ be the set of simple planar polygons with exactly $n$ vertices and diameter at most $1$, and define
```math
A_n = \sup\{\mathrm{area}(P) : P \in \mathcal{P}_n\}.
```
The problem is to determine $A_n$ for every $n$ and characterize the maximizing polygons up to Euclidean congruence, including reflection.

The odd orders were settled by Reinhardt: the regular small $n$-gon is optimal and
```math
A_n=\frac{n\sin(2\pi/n)}{8\cos^2(\pi/(2n))}.
```
For even orders, the established cases include $n=4,6,8,10,12$. In particular, $A_4=1/2$, with infinitely many noncongruent maximizers. Bingane and Mossinghoff's paper cited below records the remaining problem for even $n\geq14$.

### Recent preprint and intended scope

I am the author of *Maximum-Area Small Polygons of Even Order*, [arXiv:2608.15666](https://arxiv.org/abs/2608.15666), submitted for publication.

The manuscript states that for every even $n\geq8$ there is a unique congruence class of maximizers. It gives an exact variational characterization of the maximal area through the unique critical point of an explicit strictly concave function and an explicit geometric reconstruction. Together with the classical odd orders and the cases $n=4,6$, this would determine $A_n$ for all $n\geq3$.

I propose adding the classical problem with this preprint disclosed as a proposed solution. A complete Lean proof is not yet available. I would welcome the maintainers' guidance on the appropriate status category.

The planned contribution will distinguish the problem of determining the maximal area from the uniqueness assertion. In particular, it will preserve the quadrilateral exception. A later complete Lean proof would be hosted externally and linked through the repository's formal_proof mechanism.

### References

- C. Bingane and M. J. Mossinghoff, *Small polygons with large area*, Journal of Global Optimization 88 (2024), 1035–1050. [Published article](https://doi.org/10.1007/s10898-023-01329-1); [open manuscript](https://optimization-online.org/wp-content/uploads/2022/05/8902.pdf). The introduction reviews the classical problem and known cases.
- J. Foster and T. Szabó, *Diameter graphs of polygons and the proof of a conjecture of Graham*, Journal of Combinatorial Theory, Series A 114 (2007), 1515–1525. [Published article](https://doi.org/10.1016/j.jcta.2007.02.006).
- D. Trela, *Maximum-Area Small Polygons of Even Order* (2026). [Preprint](https://arxiv.org/abs/2608.15666).

### Prerequisites needed

Finite planar configurations, Euclidean distance, polygonal area, convex hulls, and congruence under Euclidean isometries. The repository already has EuclideanGeometry.IsConvexPolygon in FormalConjecturesForMathlib/Geometry/2d.lean. The formalization should account explicitly for the number of genuine vertices and the equivalence between the original polygon problem and a convex-hull formulation.

### AMS categories

- AMS 52 — Convex and discrete geometry
- AMS 90 — Operations research, mathematical programming

### Choose either option

- [x] I plan on adding this problem to the repository.
- [ ] This issue is up for grabs.

This issue was prepared with AI assistance.

Start by reading EuclideanGeometry.IsConvexPolygon in FormalConjecturesForMathlib/Geometry/2d.lean and the repository's formal_proof mechanism. The issue proposes adding the small-polygon problem, including genuine vertex counts, convex-hull equivalence, and the quadrilateral exception, but leaves the formalization and status category for maintainer guidance.

Written by the indexing model from the issue text.