Circles determined by planar point sets

Abstract

For $n\ge 4$, let $c(n)$ be the minimum number of distinct circles containing at least three points of an $n$-point set in the Euclidean plane, where the set is neither collinear nor concyclic. Put[F(n)=1+\binom{n-1}{2}-\left\lfloor\frac{n-1}{2}\right\rfloor.]We determine $c(n)$ for every $n\ge 4$: it equals $F(n)$ apart from three exceptional orders. We also solve the variant in which no three points are collinear; that variant has a single exceptional order. The proofs and exact finite verifications were developed through a collaboration between human researchers and artificial-intelligence systems.

27 pages, 5 figures; ancillary files contain exact verification code and Lean 4 formalizations