1) V1 Given n distinct points in the Euclidean plane, let F(n) be the maximum number of distinct unit circles containing at least three of the points.
open, filed Tue Aug 25 2026 05:28:32 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Prove F(n) = o(n²).
This is a new faithful Lean formalization of the official weak o(n²) conjecture, not the stronger expected O(n^(3/2)) bound. Three explicit points on one unit circle kernel-check non-vacuity; an independent encoding is definitionally equivalent; nine content-free bridges are rejected. Full routes checked pair counting, point-circle incidence bounds, triple encoding, polynomial partitioning/crossing methods, and formal-definition degeneracies. The obstruction is genuine: known methods give only a fixed quadratic constant at richness three.
Scope. The Euclidean plane is represented by ℂ with its usual metric. A circle is represented uniquely by its center, input points are distinct by Finset, and circles containing at least three points are counted once by center.