---

Claim. The theorem erdos_264.parts.i of the linked Lean 4 file proves ¬IsIrrationalitySequence (2 ^ ·), the formal-conjectures statement of its time that $a_n=2^n$ is not an irrationality sequence of this type, with the perturbations $b_n$ ranging over $\{1,\dots,4\}$. Boris Alexeev posted the file to Alexeev's lean-proofs repository and announced it on the site's discussion thread on 2025-12-18. The file's header says that Aristotle (Harmonic) proved the result itself, starting from the formalization already available in the Formal Conjectures project, in a run operated by Pietro Monticone; Alexeev writes in the thread that Aristotle was not given the paper of Kovač and Tao, and Kovač replied that the range $\{1,2,3,4\}$ suffices, which Kovač had not observed. The file also proves erdos_264.variants.example, that $2^{2^n}$ is an irrationality sequence of this type, a formal-conjectures variant outside both parts of the problem; Kovač notes in the thread that this case follows from a 1964 theorem of Erdős and Straus. The statement as formalized at the time took perturbations in the natural numbers; the current formal-conjectures statement takes integers, and a positive witness serves both. On 2026-08-25 the file was merged into a combined file whose header names Kovač and Tao as informal authors; that file is linked on their page.

Submission note. Posted to the site's forum by Boris Alexeev on 18 December 2025:

Aristotle was able to prove that $2^n$ is not an irrationality sequence, while $2^{2^n}$ is, directly from the formalized statements previously made available at the Formal Conjectures project. (This run was operated by Pietro Monticone a few days ago.) Type-check it online!

In particular, it was not provided with the paper by Kovač and Tao. (However, I don't know whether its argument derived from that source anyway.) In particular, I haven't looked at the proof, except to note that it mentions 1 through 4 a lot (instead of 1 through 5 as in the other proof).

Covers. The powers-of-two part, with the same answer as Kovač and Tao's accepted claim: $2^n$ is not an irrationality sequence of this type. Not covered: the factorial part.

Standing. Claimed. The proof is attributed to Aristotle, as the file's header and the thread post name it. The corpus has not built or audited the file, so the link is not formalized evidence; no review of it is recorded, and the site labels the problem OPEN.

Depends on. Nothing in this wiki.