Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Erdős Problem 97: a vertex without four equidistant neighbours

Disproved
Erdos9796Mission.problem97

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

convex-positiondiscrete-geometryerdos-97-96unit-distances

For every nonempty finite set AAA of points in strictly convex position in the Euclidean plane, there is a vertex p∈Ap\in Ap∈A such that every circle of positive radius centred at ppp contains at most three points of AAA.

∀A≠∅  ∃p∈A  ∀r>0:  ∣{q∈A:∥p−q∥=r}∣≤3.\forall A\ne\varnothing\;\exists p\in A\;\forall r>0:\;|\{q\in A:\|p-q\|=r\}|\le3.∀A=∅∃p∈A∀r>0:∣{q∈A:∥p−q∥=r}∣≤3.

The set is finite and convex-independent: each vertex lies outside the convex hull of all the others. No lower bound of three on the cardinality is imposed; singletons and two-point sets are included. This is the affirmative target of Problem 97, which remains open in the repository.

Preamble
import Definitions.Def_Erdos9796Mission

/-!
The open Erdős Problem 97 statement in the self-contained mission vocabulary.
-/
Formal statement
theorem Erdos9796Mission.problem97 : Erdos9796Mission.Problem97 := by sorry
Source
https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/UpstreamBridge.lean#L30; https://www.erdosproblems.com/97
Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

The declaration asserts that for every finite point set AAA in the Euclidean plane, if AAA is nonempty and every point of AAA is absent from the convex hull over R\mathbb{R}R of the remaining points A∖{a}A\setminus\{a\}A∖{a}, then there is at least one point p∈Ap\in Ap∈A for which no positive real radius rrr has at least four points q∈Aq\in Aq∈A at distance exactly rrr from ppp. In expanded form, for that point ppp, every r>0r>0r>0 satisfies #{q∈A:dist⁡(p,q)=r}<4\#\{q\in A: \operatorname{dist}(p,q)=r\}<4#{q∈A:dist(p,q)=r}<4. The theorem body is sorry, so this is an asserted target rather than an established result.

Human review
  • Endorsed by Shuze Chen · Sep 8, 2026

  • Endorsed by mysticflounder · Sep 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me