Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Let be a finite set whose nonzero pairwise distances take exactly values. Then ; for , every two-distance set of Problem 502 has at most points. This is the Bannai–Bannai–Stanton theorem, which has its own claim page in this folder; Petrov and Pohoata's proof is independent of the original and is recorded as a result of its own.
Covers. The part upper_bound of the corrected Statement: the bound
on every two-distance set in . With
the lower construction of points, which settles the other
part, it gives the asymptotic behavior of the largest size,
which the problem asks for.
The argument. Write over the distances . The matrix is a nonzero multiple of the identity, so its rank is , while the authors' Theorem 1.2, a real strengthening of the Croot–Lev–Pach lemma using Sylvester's law of inertia, bounds the positive and negative inertia indices of such a matrix by the dimension of the degree-at-most- polynomials restricted to , which is at most . The library's [[../library/distance_problems/petrov_2021_remark_sets_few_distances/theorem_1_1|Theorem 1.1 page]] gives the complete proof and its [[../library/distance_problems/petrov_2021_remark_sets_few_distances/theorem_1_2|Theorem 1.2 page]] the rank and inertia lemma, with the source's indexing misprint corrected there.
Formalization. The site's label carries a Lean qualification. The formal-conjectures statement of the upper bound points to a Lean 4 development in Alexeev's lean-proofs repository, linked above at a pinned commit, which declares itself a formalization of a solution to the problem with Petrov and Pohoata as its informal authors and names the AI system Aristotle from Harmonic and one further contributor as its formal authors; by its header it formalizes the Bannai–Bannai–Stanton theorem through the Croot–Lev–Pach lemma and Sylvester's law of inertia, the argument of this paper. It declares the upper bound only, not the exact maximum. This corpus has not built or audited that development, so it is a link on this page and not evidence of acceptance.
Acceptance. The paper is refereed: F. Petrov and C. Pohoata, A remark on sets with few distances in , Proceedings of the American Mathematical Society 149 (2021), no. 2, 569–571, published online 2020-11-25; the preprint is arXiv:1912.08181, posted 2019-12-17. The curator of erdosproblems.com, Thomas Bloom, marks the problem solved and credits this paper with the simple proof of the upper bound.