---

Claim. The gist Erdos1136.lean linked above (243 lines, importing Mathlib), posted to the discussion thread of Problem 1136 on 19 April 2026 by the forum user Lorenzo Luccioli, who writes that they asked Aristotle to formalize the solution to the problem and posts the code it produced, defines $A$ as the positive integers whose odd part is $3\pmod4$ and proves erdos_1136: there is a set $A\subset\mathbb N$ with $a+b\ne2^k$ for all $a,b\in A$ and $k\ge0$ and some $N_0$ with $|A\cap[1,n]|>n/3$ for every $n\ge N_0$. That statement is weaker than the question, which asks for lower density above $1/3$: a count exceeding $n/3$ for all large $n$ allows lower density exactly $1/3$. The file's lemma density_lower_bound_general, $|A\cap[1,n]|\ge3\lfloor n/8\rfloor$ for every $n$, gives lower density at least $3/8>1/3$ and so the question's answer, and the proof of erdos_1136 derives the headline bound from it with $N_0=64$; the headline theorem does not state it. The file's header names no author, no source and no prover; only the post names Aristotle. Its text contains no sorry, axiom declaration or native_decide. The page rests on the file's text at the pinned revision; nothing was built, kernel-checked or audited here.

Submission note. Posted to the site's forum by Lorenzo Luccioli on 19 April 2026:

I asked Aristotle to formalize the solution to this problem. Here is the code that was produced.

Standing. Claimed: no outside acceptance of the file exists, since the site's label PROVED (LEAN) credits Müller's construction, recorded on Müller's claim page, and no independent audit of the formal statement was made here. The set $A$ is Müller's set, but the file names no informal author, so it presents itself as an independent proof. The later Lean files of 21 April 2026, whose headers name Müller as the informal author and credit this gist as a similar formalization, are linked from Müller's page.

Depends on. No page of this wiki.