Mo Putera comments on Mo Putera’s Shortform

Mo Putera 4 May 2026 18:17 UTC
4 points
0
Update: Jared Lichtman, Terry Tao, and a few others just posted to the ArXiv this paper. Abstract:
Abstract. A set of integers is primitive if no number in the set divides another. We introduce a new method for bounding Erdős sums of primitive sets, suggested from output of GPT-5.4 Pro, based on Markov chains with von Mangoldt weights. The method leads to a host of applications, yet seems to have been overlooked by the prior literature since Erdős’ seminal 1935 paper.
As applications, we prove two 1966 conjectures of Erdős–Sárközy–Szemerédi, on primitive sets of large numbers (#1196) and on divisibility chains (#1217). The method also provides a short proof of the Erdős Primitive Set Conjecture (#164), as well as the related claim that 2 is an “Erdős-strong” prime. Moreover, the method resolves (a revised form of) the Banks–Martin conjecture, which has long been viewed as a unifying ‘master theorem’ for the area.
The acknowledgements section:
ChatGPT was used to generate code for several of the images in this paper, to search for relevant literature (for instance, in locating references for the proof of Lemma 3.2), to proofread the paper and to offer additional suggested results and remarks11, and to perform numerics to guide the proof of Lemma 3.4.
The initial proof of Theorem 1.1 was generated by an autonomous run12 of GPT-5.4 Pro; a similar run also established Theorem 1.6. GPT-5.4 Pro was also used to assist with the initial proof of Theorem 1.2, with the main human contributions being the downward divisor chain and suggesting Lemmas 3.2 and 3.3(ii) to establish the sub-invariance property. In addition, an early version of GPT-5.5 Pro was used to assist with the initial proof of Theorem 1.3. Finally, GPT-5.4 Pro helped prove Theorem 1.4. Nevertheless, the final proofs in this paper have been generated and reviewed by the human authors, using the AI-generated proofs as starting points when appropriate.
The Lean formalization in [2] was generated using OpenAI’s Codex. The Lean formalization in [33] was generated using Math Inc.’s Gauss.