Back to Problems

erdos_97.variants.three_unit_distance

Specification

Fishburn and Reeds [FiRe92] have found a convex polygon on 20 points such that every vertex has three vertices equidistant from it (and this distance is the same for all vertices). [FiRe92] Fishburn, P. C. and Reeds, J. A., _Unit distances between vertices of a convex polygon_. Comput. Geom. (1992), 81-91.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
theorem erdos_97.variants.three_unit_distance :
    ∃ A : Finset ℝ², A.Nonempty ∧ ConvexIndep A ∧ HasNUnitDistanceProperty 3 A
ID: ErdosProblems__97__erdos_97.variants.three_unit_distance
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.