Erdős Problem 506 asks for the minimum number f(n) of distinct circles determined by n planar points that are neither all collinear nor all concyclic. The recently completed classification relies on long arguments, some of them computer-assisted.

For n=8, an inversion argument is combined with a seven-point lemma bounding three-point lines when no four points are collinear. For n≥15, Melchior's inequality and Langer's incidence bound give a single weighted-line inequality covering the whole range. The remaining finite cases are cited from other work. The full classification is formalized in Lean 4 in Wrona's credited repository, and Wang's Lean files formalize an arithmetic layer of a related proof.

Short proofs are given that f(8)=17, attained by an explicit configuration, and that f(n)=1+C(n-1,2)-⌊(n-1)/2⌋ for every n≥15. The n=8 proof needs no computer-assisted classification of incidence types.