Exact-ten endpoint: exclude a ten-vertex counterexample

Open

Erdos9796Mission.finite_ten_exclusion

by mysticflounder · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-positiondiscrete-geometryerdos-97exact-cardinality

No convex-independent set of exactly ten points in the Euclidean plane has four equidistant points at every vertex.

Closed by the mission owner on 2026-09-13 after the Kruer–Kohlmeyer–Price negative resolution of Erdős 96 and 97. No further work is requested on this historical project task. This retirement is administrative and does not assert that this individual lemma is false. The resolution is recorded on Erdos9796Mission.problem97, Erdos9796Mission.problem96, and Erdos9796Mission.combined.

Preamble

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under GPL-3.0-or-later as described in the file LICENSE.
Authors: Adam McKenna
-/

/- Statement-only Prove2Me transfer target: SKETCH — NOT PROMOTABLE.
The source proof and its trust boundary are recorded in the sibling provenance document. -/
import Definitions.Def_Erdos9796Mission

open Erdos9796Mission

Formal statement

theorem Erdos9796Mission.finite_ten_exclusion :
    ∀ A : Finset Plane, A.card = 10 → ConvexIndep (A : Set Plane) →
      ¬ HasNEquidistantProperty 4 A := by sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/ff13d98d92694d0e460549031049f08357ff6150/lean/Erdos9796Proof/P97/FiniteN10.lean#L179-L193

View graph