2026-09-25 · article combinatorial geometryErdős problemsLean 4

Four points with distinct circumradii — n4 = 7

Erdős Problems (erdosproblems.com) is a website that collects, by number, the problems left by the mathematician Paul Erdős. This article is about problem 827 there (#827 below; https://www.erdosproblems.com/827). The question: how many points in the plane are needed to be sure of finding four of them such that the four triangles made from them, one for each choice of three of the four points, all have different circumradii (the circumradius of a triangle is the radius of the circle through its three vertices)? The answer is 7. The problem was already solved — the value was recorded on the site's discussion forum on 22 September 2026 — and the author of that record asked for verification by others. This article comes after it: an independent verification, by a different route, in which a proof of n4 = 7 is written in Lean 4 (a proof assistant that checks proofs by machine) and passes its check from end to end.

Leanmachine-checked (Lean 4, no sorry, no native_decide; axioms a subset of propext, Classical.choice, Quot.sound; theorem names given) paperproved but not yet machine-checked computedverified on this machine only; not put forward as a claim knownknown theorem, restatement, or a check against the literature

This page says nothing about how fast nk grows. It concerns one value, k = 4, in the plane. The best known asymptotic bounds (the behaviour for large k) are listed in §02 and are untouched by anything here.

Let nk be minimal such that if nk points in R2 are in general position then there exists a subset of k points such that all C(k,3) triples determine circles of different radii. Determine nk.

Erdős problem #827, as stated on the problem page.

General position is taken here in Erdős's own sense for this problem.known

The third condition matters. The upper bound below uses "no three collinear" in three places inside the argument, so under the weaker convention of Martínez and Roldán-Pensado, which allows three collinear points, this chain yields only 7 ≤ n4 ≤ 9. The value depends on the convention.

Write out the quantity for k = 4. Four points a, b, c, d determine four triangles, one for each omitted vertex: bcd, acd, abd, abc. Call the 4-set good if these four circumradii are pairwise different. Call N a good size if every N points in general position contain a good 4-subset; n4 is the least good size. A configuration in general position with no good 4-subset is called bad.

The forum record adds a reservation of its own about the upper bound: that it rests on Singular, on a SAT solver and on five hand lemmas about radius classes from notes on another problem; that the second implementation which redid every step was AI-assisted too, so it is a re-check of the same author's work rather than independent review; and that someone else should run it. The proof on this page is a different route at every stage — a different enumeration, a different refutation, a different algebraic model, no SAT solver, no computer algebra system, and none of those hand lemmas — and the whole chain that reaches the same value is checked by the Lean kernel. It is the independent, machine-checked confirmation that was asked for. What it is not is an audit: no computational step of that record has been re-run or inspected here.Lean

A useful change of view: call a set circle-Sidon if all its triples determine circles of different radii. Phrased that way the probabilistic bound is the classical Sidon-set deletion argument, and it says that n points contain a circle-Sidon subset of size ≫ n1/5.known

The Lean statement:Lean

theorem sInf_isGood_eq_seven : sInf {N : ℕ | IsGood N} = 7

There are four definitions, each a transcription of the geometry. Pt is ℝ × ℝ, sqdist is squared distance, cross a b c is twice the signed area, and det4 is the determinant that vanishes when four points lie on one circle or one line.

def GeneralPosition {N : ℕ} (p : Fin N → Pt) : Prop :=
  (∀ i j : Fin N, i < j → p i ≠ p j) ∧
  (∀ i j k : Fin N, i < j → j < k → ¬ Collinear3 (p i) (p j) (p k)) ∧
  (∀ i j k l : Fin N, i < j → j < k → k < l → ¬ Concyclic4 (p i) (p j) (p k) (p l))

def CircumRadiusSq (a b c : Pt) (r : ℝ) : Prop :=
  ∃ o : Pt, sqdist o a = r ∧ sqdist o b = r ∧ sqdist o c = r

def FourDistinct (a b c d : Pt) : Prop :=
  ∀ i j : Fin 4, i ≠ j → ∀ r s : ℝ, face a b c d i r → face a b c d j s → r ≠ s

def IsGood (N : ℕ) : Prop :=
  ∀ p : Fin N → Pt, GeneralPosition p →
    ∃ i j k l : Fin N, i < j ∧ j < k ∧ k < l ∧ FourDistinct (p i) (p j) (p k) (p l)

Four things are worth reading off. (1) p is a map, but the first clause of GeneralPosition makes it injective, so it really is N distinct points. (2) Indices are taken in increasing order, so each subset is tested once. (3) Circumradii appear squared; radii are non-negative, so distinctness of the squares is distinctness of the radii. (4) CircumRadiusSq is existential ("some centre is at squared distance r from all three"), so the existence of a circumcircle is not assumed; in general position three points are never collinear, so it exists and is unique.

One six-point set with integer coordinates gives n4 ≥ 7. The configuration in the Lean files is:Lean

It is in general position, and each of its fifteen 4-subsets contains two triangles of equal circumradius. Rational arithmetic suffices to check this, and that is what the formal proof does (seven_le_sInf_isGood_and_sInf_isGood_le_nine).

Its shape

Rearranged about (2,3), the set is centrally symmetric (there is a point O such that the reflection of every point through O is also in the set):

Call this shape octahedral: the six points split into three pairs and the eight transversal triangles — those taking one point from each pair — all have the same circumradius. The eight faces of an octahedron are where the name comes from. In Lean:

def OctahedralSix (q : Fin 6 → Pt) : Prop :=
  ∃ (e : Fin 3 → Fin 2 → Fin 6) (r : ℝ),
    Function.Bijective (fun p : Fin 3 × Fin 2 => e p.1 p.2) ∧
    ∀ a b c : Fin 2, CircumRadiusSq (q (e 0 a)) (q (e 1 b)) (q (e 2 c)) r

Why such a set is bad

Write the six points as three pairs {±u, ±v, ±w}, putting the centre at the origin. A 4-subset falls into exactly two cases.paper

• It contains two whole pairs, say {u, −u, v, −v}. That is a centrally symmetric parallelogram, and the two triangles on one side and the other of a diagonal are exchanged by the point reflection through the centre, hence congruent, hence of equal circumradius.
• It contains one whole pair and one point from each of the others, say {u, −u, v, w}. Then the triangles u v w and −u v w are both transversal, so their circumradii agree by the octahedral condition.

Either way some pair of triangles repeats a circumradius, so the set is bad, and six points do not suffice: n4 ≥ 7.

When octahedral sets occur

Reading the points as complex numbers {±a, ±b, ±c}, the set is octahedral exactly when the squares a2, b2, c2 are collinear. In real coordinates the same condition is Σ (a·b)(a×b) = 0, summed over the three pairs. Geometrically: the six points lie on one rectangular hyperbola as three pairs of antipodes.paper

For the integer set above, a = (2,3), b = (1,1), c = (1,0), and the squares are (−5,12), (0,2), (1,0) — collinear. The hyperbola is x2 + xy − y2 = 1 translated by (2,3). The family has three parameters and plenty of rational members.

The upper bound is the work of exhausting the shapes of bad six-point sets. The chain has five steps, all of them in Lean.Lean

Steps 1–3 give "every bad six-point set in general position is octahedral" (octahedralHypothesis); with steps 4 and 5 this yields IsGood 7, that is n4 ≤ 7. With the lower bound, n4 = 7.

The core of step 4 — a sum of circumcentres

This step alone is a short identity. If two circles of the same radius R pass through two distinct points u, v, their centres are symmetric about the midpoint of u v, so the two centres sum to u + v. Read backwards: if two triangles share the edge u v and have the same circumradius, their circumcentres (the centres of their circumcircles) add up to u + v. In an octahedral set there are four transversal triangles through any one vertex, and four applications of this identity produce the point symmetry. Only six of the eight transversal triangles are used.Lean

The shape of step 5

If a seven-point set were bad, then deleting each point in turn leaves seven bad 6-subsets, each of which is centrally symmetric by steps 1–4. For a seven-point set with no three collinear this is impossible. This is one of the places where "no three collinear" is used, and it is why weakening the convention breaks the argument.Lean

Cells and witnesses

To record where a six-point set has equal circumradii, use cells. A cell is a pair (two apexes, one shared edge): fifteen ways to choose the apexes, six ways to choose an edge among the remaining four points, so there are 90 cells. The cell ((c,d),(a,b)) stands for the two triangles a b c and a b d sharing the edge a b.

Equality of their circumradii is the vanishing of one polynomial.Lean

In general position — using that the four points are not concyclic — Ψ = 0 ⟺ the two circumradii are equal. A cell where Ψ vanishes is a witness, and the witness set is a 90-bit mask. A configuration p carries a mask w when the set of vanishing cells is exactly w.

Ψ has a second face: it is exactly 16 times the determinant expressing that the four midpoints mid(a,b), mid(a,c), mid(b,c), mid(c,d) are concyclic. Geometrically: the midpoint of c d lies on the nine-point circle (the circle through the midpoints of the three sides) of the triangle a b c.Lean

Badness is a statement about witnesses: each of the fifteen 4-subsets carries at least one. The converse question — given a mask, is there a six-point set in general position carrying it? — is the work of the next two sections.

The coordinate route — membership in a radical

The direct approach is to write the equations and show they have no solution. Once the witness set is fixed, the conditions Ψ = 0 are a system of polynomial equations. Substituting the forced midpoint relations reduces the unknowns (to four if the set is centrally symmetric, to six if there is one parallelogram), and then the ideal (the set of all polynomials obtainable from the equations by addition and multiplication by polynomials) is saturated by the 20 collinearity determinants and the 15 concyclicity determinants — that is, the degenerate solutions, where three points would become collinear or four concyclic, are divided out.

If what is left is ⟨1⟩ (the ideal contains 1, so it is the whole polynomial ring), there is no configuration even over the complex numbers: equivalently, 1 lies in the radical (the set of polynomials some power of which lies in the ideal), with a certificate. Ten of the 34 types fall this way.

The orientation route — ζij

The coordinate route stalls as degrees rise; for some types the elimination does not terminate. So change to angles. Reading points as complex numbers and fixing an edge c d, set

Then Ψ(c,d;a,b) is the cross product of w(a) and w(b), and equality of circumradii becomes δcd(a) = δcd(b): a witness is a linear condition on orientations. In that form, witnesses over a common edge are automatically transitive, two complementary witnesses force two lines to be parallel or perpendicular, and so on — all without returning to the geometry.Lean

For the actual refutations the orientations are normalised, wij = ζij / ζ01. A cell condition then reads wac wad = wbc wbd and collinearity reads wab = wac: multiplicative relations, hence, in the exponents, linear algebra over an integer lattice. Computing elementary divisors (the diagonal entries after an integer matrix is diagonalised) reduces the remaining freedom to a finite case check. Twenty types fall by the orientation route, and four more by the orientation route with the lattice.

One observation that made those last four work: on the branch f = ±1 the three triangle radii satisfy r2 = r1 r3, which forces one of them to be 1 — that is, three points collinear. So a single triangle suffices, and no parametrisation is needed; the degree drops from 105 to 13.

Step 1 — the witness set is one of 35 types — means exhausting a space of 90-bit masks. Listing all 290 is out of the question, so a search tree (case distinctions arranged as branches) is grown instead.

A node records which cells have been decided to be witnesses (pos) and which have been decided not to be (neg). The root decides nothing. The available moves are:

The tree is exhausted: 204,890 nodes in 1,820 subtrees, with no leftovers and no open leaves.Lean

To carry the tree into Lean, each theorem is stated in the form "this node is settled once the nodes handed off from it are", the nodes are ordered deepest-first, and they are cut into 73 files each importing the previous one. The last file holds theorem censusComplete. Measured on the Lean side: 74 files, 15,955 seconds in total, and all 1,842 lines of axiom output are subsets of the three standard axioms.

What finally exhausted the tree was the move that maps a node to a normal form under a permutation. Without it the handed-off nodes never run out. No new geometry is involved; what is needed is that renaming the four points does not change whether a circumradius repeats.

The namespace is DistinctCircumradii. There is no sorry and no native_decide (a device that hands part of a proof's computation to compiled code and skips the kernel's check), so the check closes inside the Lean kernel (the small core that gives a proof its final check) and nothing depends on computation outside it. The axiom output for the main theorems (#print axioms, the command that prints the axioms a theorem rests on) is these four lines:

'DistinctCircumradii.restUnrealizable'     depends on axioms: [propext, Classical.choice, Quot.sound]
'DistinctCircumradii.octahedralHypothesis' depends on axioms: [propext, Classical.choice, Quot.sound]
'DistinctCircumradii.isGoodSeven'          depends on axioms: [propext, Classical.choice, Quot.sound]
'DistinctCircumradii.sInf_isGood_eq_seven' depends on axioms: [propext, Classical.choice, Quot.sound]

The fourth line reaches the whole chain: sInf_isGood_eq_seven depends through censusComplete on all 74 search-tree files, so that single line certifies that nowhere in the chain is there a sorry or an extra axiom.

Where the sources are

The Lean sources for this article are in the bundle principia-src.tar.gz (top-level directory principia/; Lean 4 v4.33.1 with Mathlib). The modules are the 100 files Principia.DistinctCircumradii.*; the main theorem is DistinctCircumradii.sInf_isGood_eq_seven in Principia/DistinctCircumradii/Final.lean; the axioms are the three propext, Classical.choice and Quot.sound. The sha256 of the bundle is 131d8da3426838ca717991bf642551ee8fa5e2656c4952fb1babf050bd175c1b, and the axiom output is in axioms-principia.txt.

Rebuilt independently

The finished proof was then rebuilt away from the environment that produced it: the 25 linked modules and Final were copied from the originals (md5 sums taken before and after, and unchanged), and the olean files (the checked intermediate files Lean writes) were regenerated one at a time. All 26 returned 0 with empty standard error and no sorry or native_decide; the axiom output ran to 549 lines, every one a subset of the three standard axioms (505 with all three, 37 with propext and Quot.sound, 7 with propext alone). The 74 search-tree files were rebuilt the same way and all passed.Lean

The transformation itself was checked mechanically too. The linked version was produced from a state in which each file carried its own copy of the shared base, by deleting the copies and replacing them with imports. A separate program verified that all 667 retained declarations are literally identical, comments aside, to the declarations of the same name in the originals. Three auxiliary lemmas were renamed to avoid clashes; no statement of a main theorem was touched.

What is said and what is not

What is in Lean is the whole chain. The lower-bound configuration, the exhaustiveness of the search tree, the non-realisability of the 34 types and the lift to seven points all sit under one statement. That is the difference from the earlier pages, where a finite core was machine-checked and the rest was left on paper.

What is not claimed:

• Nothing about k ≥ 5. The chain is about k = 4, and the 90-cell structure is specific to it.
• The plane only (ℝ × ℝ). No higher-dimensional analogue is treated.
• It depends on the convention. Allowing three collinear points, the chain gives only 7 ≤ n4 ≤ 9.
• Nothing about the growth of nk. The gap between the known O(k5/log k) and k2−o(1) is untouched.
• The proof is not in human-readable form. The 204,890 nodes of the search tree are for Lean to read.

Known facts used

What this page adds

The chain here was built without reference to the forum comment mentioned at the top, and uses different tools (SAT and saturation in Singular there; a search tree and proof terms inside Lean here). What it adds is the following.

The independent check that the forum record asks for (§02) is answered here by a different route: a different enumeration, a different refutation and a different algebraic model, with no SAT solver, no computer algebra system and none of those hand lemmas, reaching the same value under machine check. The computational steps of that record have not been re-run or audited here. What agrees is the value, not two computations compared step by step.

Range searched: the problem page and every comment on its forum, plus the bibliographic data of the works above. Citation lists were not followed. For the rows above that were not found in that range, the most that can be said is "not found in the range searched".

• The same route does not reach n5. The analogue of steps 1–4 — "a bad set is centrally symmetric" — is false at k = 5: there are eight-point sets in which every 5-subset repeats a circumradius and which are not centrally symmetric. Deciding k = 5 needs a different skeleton.
• The gap between conventions is open. Under the weaker convention n4 is 7, 8 or 9, and this chain does not say which. The three places where "no three collinear" is used would have to be rewritten to cover the collinear cases.
• The proof is too large. A search tree of 204,890 nodes is not something a person reads. There ought to be a shorter reason why a bad six-point set is octahedral — central symmetry comes out at the end, which suggests an argument that produces the symmetry first, but none has been found.
• It has not been checked by an independent third party. The checks described here rebuild the same proof in another environment; they are not someone else verifying it with other tools. The Lean sources are in the bundle linked in §08.

References