A convex independent K4 configuration is not collinear

Proved

Batch3N9.Problem97.not_collinear_of_K4

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

A nonempty convex-independent finite planar set with the four-point equidistance property cannot be collinear.

Preamble

import Definitions.Def_Erdos9796FiniteNine_N8Interface
import Mathlib.Analysis.Convex.Independent
import Mathlib.Data.Finset.Filter
import Mathlib.Geometry.Euclidean.Sphere.Basic
import Mathlib.Tactic.NormNum
open scoped EuclideanGeometry
open Finset

Formal statement

theorem Batch3N9.Problem97.not_collinear_of_K4 {A : Finset ℝ²} (hne : A.Nonempty) (hconv : ConvexIndep A) (hK4 : HasNEquidistantProperty 4 A) : ¬ Collinear ℝ (A : Set ℝ²) := by sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/N9Endpoint/Closure.lean

View graph