---

Claim. There is an infinite Sidon set of positive integers that is an asymptotic basis of order three, the theorem of Pilatte, proved by a different route. The result was first posted on 2026-08-25, when Boris Alexeev's Lean repository gained the development Erdos157.lean, whose repository page calls it a formalized proof of Problem 157; its unconditional theorem Erdos157.erdos_157 proves an earlier form of this construction, with coefficients in the field of $2^{1024}$ elements. The write-up's version over $\mathbb{F}_2$ is the theorem Erdos157.Binary.erdos_157 of the file Erdos157b.lean, committed on 2026-08-26. The same result was then posted twice more: the write-up A Sidon basis of order three from polynomials over $\mathbb{F}_2$ (PDF of 2026-09-15, which prints no author) and, the same day, an entry on the site's proof-claims page for Problem 157 by the forum user BorisAlexeev, who writes that they asked the AI system GPT-6 Astra to solve the problem without the hard-to-formalize literature results that Pilatte's proof uses, and who describes the write-up as rough. The write-up keeps Pilatte's encoding of irreducible polynomials by discrete logarithms but lets the target residue class vary: each block carries a tag from a finite field of characteristic seven, recorded with its square, and a shared random shift of the discrete logarithm, so the Sidon property survives while triples gain many independent attempts to land in a class rich in prime products. The only distribution estimate used is an elementary zero-free region for polynomial Dirichlet $L$-functions over $\mathbb{F}_2[t]$; Sawin's estimate and the Riemann hypothesis for curves are not used. A single Borel–Cantelli argument over one product space gives the basis property.

Submission note. Posted to erdosproblems.com as a proof claim by GPT-6 Astra (account BorisAlexeev) on 15 September 2026, giving "GPT-6 Astra" as the AI used:

Recently I attempted to unconditionally formalize all known solutions to Erdős problems. The existing solution to this problem by Pilatte uses a result of Sawin which itself uses the solution to the Weil conjectures. While I think auto-formalization is here, and I think it is possible to auto-formalize that today (given enough time), I sought an easier path to formalization. So instead, I asked GPT-6 Astra to solve the problem in a different way, without using difficult-to-formalize results from the literature. I'm sorry for the slop writing. This is actually after a few iterations of attempted improvement.

Depends on. No page of this wiki.

Acceptance. Formalized. This corpus's verification built the module ErdosProblems.Erdos157 of the repository at its commit of 2026-09-15, the first formalization link above (Lean v4.33.0, Mathlib v4.33.0), and checked the axioms of Erdos157.erdos_157, which are exactly propext, Classical.choice and Quot.sound. The repository's comparator challenge ComparatorChallenges/ErdosProblems/Erdos157.lean pins that theorem together with the two definitions its type reaches, Erdos157.IsSidon and Erdos157.IsAsymptoticBasisOfOrderThree, and the fingerprint of the built declaration was found identical to the challenge. The statement was audited clause by clause against the problem's Statement: it asserts an infinite set $S\subseteq\mathbb{N}$ that is Sidon in the full sense, the case $a=b$ included, and a threshold $N_0$ beyond which every integer is $a+b+c$ with $a,b,c\in S$, repeats allowed, which is the site's question answered yes. Allowing $0\in S$ costs nothing, since $S+1$ keeps all three properties and gives the positive-integer form stated above. The theorem is proved in the development's module Unconditional.lean, not from its conditional theorems along Pilatte's route, each of which takes a hypothesis from Sawin's geometry. What was built is the earlier form of the construction, over the field of $2^{1024}$ elements, in a later revision of the file first posted on 2026-08-25 (the second formalization link); it is not the write-up's version over $\mathbb{F}_2$. Erdos157b.lean is a separate theorem and not a standalone file: at its pinned commit its submodules import seventeen modules of ErdosProblems/Erdos157/, and its proof calls Erdos157.infinite_of_isAsymptoticBasisOfOrderThree. It was not built here. Not reviewed: the proof-claims entry had no comments and the site's curator credits the problem to Pilatte, not to this proof. Not refereed: the write-up is an unpublished PDF. Pilatte's refereed theorem settles the problem as well.