Claims

../

2026_06_14_kuhn: Kuhn's thread post and repository give connected triangle-free graphs on n vertices needing at least (1-eta)n added edges to reach diameter at most four while staying triangle-free, for every positive eta and all large n; Lean proof.

---