---

Claim. Marzo and Mas, Discrepancy of minimal Riesz energy points, Constr. Approx. 54 (2021), no. 3, 473–506 (arXiv:1907.04814, posted 2019-07-10), bound the spherical cap discrepancy of the $N$-point minimizers $X_N$ of the Riesz $s$-energy on $S^d$ for $0\le s<d$. Theorem 1.1 gives

$$\sup_D\left\lvert\frac{\#(X_N\cap D)}{N}-\widetilde{\sigma}(D)\right\rvert \lesssim N^{-\frac{2}{d(d-s+1)}}\ \ (0\le s\le d-2),\qquad \lesssim N^{-\frac{2(d-s)}{d(d-s+4)}}\ \ (d-2<s<d),$$

with constants depending only on $d$ and $s$, the supremum over all spherical caps $D$ and $\widetilde{\sigma}$ the normalized surface measure. The logarithmic case $s=0$ is the energy whose minimizers maximize the product of all pairwise distances, so for $d=2$ the first exponent gives cap discrepancy $\lesssim N^{-1/3}$: the $n$-point maximizers of Problem 991 have $\max_C\lvert\lvert A\cap C\rvert-\alpha_C n\rvert\ll n^{2/3}$, which is $o(n)$. The authors present Theorem 1.1 as making quantitative the known fact that the minimizers become equidistributed as $N\to\infty$. The method passes from the cap discrepancy to a Sobolev discrepancy of a smoothed counting measure, bounded through the asymptotics of the minimal energy; the authors attribute this approach, and the $N^{-1/3}$ bound for $d=2$, $s=0$, to an unpublished manuscript of Wolff, Fekete points on spheres, which their Remark 4.3 dates to around 1992 and sketches. Wolff's manuscript has no posting, so it is recorded here and has no claim page of its own. The source card marzo_2021_discrepancy_minimal_riesz_energy_points holds the paper and its digest.

Formalization. A public Lean 4 development in Boris Alexeev's lean-proofs collection, Erdos991.lean at the commit of 2026-09-15 (the file entered the repository on 2026-08-17), declares itself a formalization of a solution to the problem, names Jordi Marzo and Albert Mas as its informal authors and Codex and GPT-5.6 Sol as its formal authors. Its theorem erdos_991 states that every sequence of $n$-point subsets of $S^2$ maximizing the product of pairwise chordal distances has spherical-cap discrepancy $o(n)$, the cap area taken as the normalized surface measure; it proves the qualitative statement only, with no rate, and so not the $n^{2/3}$ bound. Its route goes through finite positive-kernel and Stolarsky identities shared with the collection's file for Problem 988, not through the paper's Sobolev-discrepancy method. Not built or audited here: the formalization is a link and not acceptance evidence.

Depends on. Nothing in this wiki; the result rests on the cited paper alone.

Acceptance. Refereed: Constr. Approx. 54 (2021), 473–506, published online 2021-04-08. Reviewed: the site's curator, T. F. Bloom, lists the problem as proved on the strength of this paper and of Brauchart 2008, reading the $d=2$, $s=0$ case of Theorem 1.1 as a proof of the $n^{2/3}$ bound and noting the earlier unpublished bound of Wolff (site page last edited 2025-09-16). This corpus has not reproduced the proof; the standing rests on the refereed paper and the site's acceptance. The rate improves Brauchart's $O(n^{3/4})$; both results settle the question.