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.

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