The weak pinned planar distance theorem

Lean formalization in OpenAI math repository (Result 167)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'The weak pinned planar distance theorem'. We prove the weak pinned Erdős distinct-distance conjecture. For every fixed ε > 0, all but o(n) points of any n-point planar set determine at least n^{1-\varepsilon} distinct nonzero distances.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 167). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository