506.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 506

References:

erdosproblems.com/506
[El67] Elliott, P. D. T. A., On the number of circles determined by $n$ points, Acta Math. Acad. Sci. Hungar. (1967), 181–188.
[BaBa94] Bálintová, A. and Bálint, V., On the number of circles determined by $n$ points in the Euclidean plane, Acta Math. Hungar. (1994), 283–289.
[PuSm] Purdy and Smith. No reference found.

Imports (1)

FormalConjecturesUtil

def Erdos506.numCircles The number of circles determined by a set of points P in the plane: the number of distinct circles (spheres) passing through at least three of the points of P line 44 source
Source documentation
The number of circles determined by a set of points P in the plane: the number of distinct circles (spheres) passing through at least three of the points of P. (Three distinct points lie on a common circle precisely when they are not collinear, so this counts exactly the circumcircles of the non-collinear triples of P.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Set.ncard, EuclideanGeometry.Sphere, ENNReal, Set.ofPred, LE.le, And, Membership.mem
14 instances, coercions and auxiliary constants left out.
```
noncomputable def numCircles (P : Set ℝ²) : ℕ :=
…
```
theorem Erdos506.erdos_506 What is the minimum number of circles determined by any $n$ points in $\mathbb{R}^2$, not all on a circle? sorry line 64 source
Source documentation
What is the minimum number of circles determined by any $n$ points in $\mathbb{R}^2$, not all on a circle?
There is clearly some non-degeneracy condition intended here - probably either that not all the points are on a line, or the stronger condition that no three points are on a line.
The answer is known for $n > 393$ (see erdos_506.variants.large_n) but the problem appears to remain open for small $n$ (see erdos_506.variants.small_n).

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, IsLeast, Set.ofPred, Exists, Finset, EuclideanSpace, Real, Fin, And, Eq, Finset.card, Not, Collinear, ENNReal, EuclideanGeometry.Cospherical, Erdos506.numCircles, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
68 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_506 (n : ℕ) (hn : 4 ≤ n) :
    IsLeast { k : ℕ | ∃ P : Finset ℝ²,
        P.card = n ∧ ¬ Collinear ℝ (P : Set ℝ²) ∧ ¬ Cospherical (P : Set ℝ²) ∧
        numCircles (P : Set ℝ²) = k }
      answer(sorry) := by
…
```
Mentions: Erdos506.numCircles
theorem Erdos506.erdos_506.variants.large_n Documented declaration: large_n sorry line 78 source
Source documentation
For $n > 393$ the answer is $\binom{n-1}{2} + 1 - \left\lfloor \frac{n-1}{2} \right\rfloor$ (Elliott [El67], with the correction of Purdy and Smith [PuSm], also reported in [BaBa94]): this is both a lower bound for every such configuration and is attained, e.g. by a circle with $n - 1$ points together with a single point off the circle.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, IsLeast, Set.ofPred, Exists, Finset, EuclideanSpace, Real, Fin, And, Eq, Finset.card, Not, Collinear, ENNReal, EuclideanGeometry.Cospherical, Erdos506.numCircles, HSub.hSub, HAdd.hAdd and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
82 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_506.variants.large_n (n : ℕ) (hn : 393 < n) :
    IsLeast { k : ℕ | ∃ P : Finset ℝ²,
        P.card = n ∧ ¬ Collinear ℝ (P : Set ℝ²) ∧ ¬ Cospherical (P : Set ℝ²) ∧
        numCircles (P : Set ℝ²) = k }
      answer((n - 1).choose 2 + 1 - (n - 1) / 2) := by
…
```
Mentions: Erdos506.numCircles
theorem Erdos506.erdos_506.variants.small_n The problem appears to remain open for small sorry line 91 source
Source documentation
The problem appears to remain open for small $n$: Elliott's answer is established only for $n > 393$, so the minimum number of circles determined by $n$ points, not all on a line and not all on a circle, is unknown for $n \le 393$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, IsLeast, Set.ofPred, Exists, Finset, EuclideanSpace, Real, Fin, And, Eq, Finset.card, Not, Collinear, ENNReal, EuclideanGeometry.Cospherical, Erdos506.numCircles, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
68 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_506.variants.small_n (n : ℕ) (hn : 4 ≤ n) (hn' : n ≤ 393) :
    IsLeast { k : ℕ | ∃ P : Finset ℝ²,
        P.card = n ∧ ¬ Collinear ℝ (P : Set ℝ²) ∧ ¬ Cospherical (P : Set ℝ²) ∧
        numCircles (P : Set ℝ²) = k }
      answer(sorry) := by
…
```
Mentions: Erdos506.numCircles
theorem Erdos506.erdos_506.variants.segre_n_eq_eight Segre's observation: the lower bound $\binom{n-1}{2}$ (without the correction of [PuSm]) is already false for $n = 8$, as witnessed by the projection of a cube onto a plane sorry line 104 source
Source documentation
Segre's observation: the lower bound $\binom{n-1}{2}$ (without the correction of [PuSm]) is already false for $n = 8$, as witnessed by the projection of a cube onto a plane. Hence the minimum number of circles determined by $8$ such points is strictly less than $\binom{7}{2} = 21$.

depends on sorry what this means
Statement uses: Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Eq, Finset.card, Not, Collinear, ENNReal, EuclideanGeometry.Cospherical, LT.lt, Erdos506.numCircles, Nat.choose, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
72 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_506.variants.segre_n_eq_eight :
    ∃ P : Finset ℝ²,
      P.card = 8 ∧ ¬ Collinear ℝ (P : Set ℝ²) ∧ ¬ Cospherical (P : Set ℝ²) ∧
      numCircles (P : Set ℝ²) < (8 - 1).choose 2 := by
…
```
Mentions: Erdos506.numCircles