A Conditional Fourteen-Point Case of Erdős Problem 132

Source: doi:10.37236/8565, url:https://www.erdosproblems.com/132 Authors: Egor Lyfar Status: verified Main declarations: LeanPool.Erdos132N14.erdos132_for_fourteen_of_published_inputs Tags: discrete-geometry, few-distance-sets, erdos-problems, planar-configurations MSC: 52C10, 05D99

A conditional fourteen-point case of Erdős Problem 132

This project formalizes the planar Hopf--Pannwitz diameter bound and proves the n = 14 conclusion conditional on exactly two remaining published interfaces: the known maximum cardinalities of planar sets with at most six distances and the Szöllősi--Östergård thirteen-point classification. The exact six-distance cardinality result is due to Wei. The general problem remains open.