P93 sum of radii in a triangle: n = 1–11 and 15
A computer-assisted proof by zzzcy, written with AI assistance: the continuous optimum is reduced to finitely many contact graphs and solved, then a localisation theorem and exact rational certificates exclude every higher score on the nine-decimal grid. The site replayed every certificate with its own code. In all twelve rows the current record is the highest grid score, and the record holders stay the same (+2 proof award).
P05 squares in a circle: n = 3, 5, 6, 7
The-Anh Vu-Le formalised in Lean 4 with Mathlib the smallest circle holding 1–7 unit squares. Citing the repository, the site marks these four rows proven optimal (n = 4 was already proved).
Discussions and mailbox: nine instances
The full-tiling area argument for P89 n = 4, 8, 16, 18 and P91 n = 12, 27, the projection argument for P90 n = 1, the centroid lemma for P82 (m = 6, n = 3), and the tightening-strip proof for P17 n = 6.
Submitting a proof
Post a proof in the problem’s discussion, or email a larger computer-assisted one. Each adopted new argument earns its contributor one +2 proof award.