---

Submission note. Posted to the site's forum by Kenta Kitamura on 22 June 2026:

I made a Lean formalization attempt for the following upper bound in Erdos Problems #536: $|A| \le N-\lfloor N/6 \rfloor$ Equivalently, this is $|A| \le \lceil 5N/6\rceil$; asymptotically, the coefficient is $5/6 \approx 0.833333$, i.e. about $0.833333N$. Here $A \subseteq \{1,\ldots,N\}$ has no three distinct elements $a,b,c$ such that $\operatorname{lcm}(a,b)=\operatorname{lcm}(a,c)=\operatorname{lcm}(b,c)$.

Lean4Web: https://live.lean-lang.org/#url=https://raw.githubusercontent.com/KitaKen1/erdos536-lean-five-six-bound/main/Erdos536_lean4web.lean Github: https://github.com/KitaKen1/erdos536-lean-five-six-bound Verification: the GitHub repository builds with 'lake build'; the checked 'Erdos536/' sources contain no 'sorry', 'axiom', or 'admit'; and the target theorem's axiom printout lists only the usual Lean foundations: '[propext, Classical.choice, Quot.sound]'.

AI usage: this Lean formalization and forum comment were prepared with assistance from Codex 5.5 using xhigh reasoning and ChatGPT 5.5 Pro.

The claim. If $A\subseteq\{1,\ldots,N\}$ has no three distinct elements $a,b,c$ with $[a,b]=[a,c]=[b,c]$, then $|A|\le N-\lfloor N/6\rfloor$; hence $f(N)\le(5/6+o(1))N$ for the function of Problem 536. The repository's target theorem is Erdos536.five_six_bound_target. The argument writes $n=m2^i3^j$ with $(m,6)=1$; for fixed $m$ the exponent pairs of an admissible set contain no corner $\{(i,j),(i-a,j),(i,j-b)\}$ with $a,b>0$, so a projection to the axes is injective and bounds the set by the integers up to $N$ not divisible by $6$.

Covers. The upper-bound constant $5/6$ only; neither $f(N)=o(N)$ nor the order of $f(N)$ is settled.

Claimant and postings. Kenta Kitamura (forum account KentaKitamura, GitHub account KitaKen1) posted the development in the site's thread on 22 June 2026, reporting that it builds with lake build, contains no sorry, axiom or admit, and that the target theorem's axiom printout lists only propext, Classical.choice and Quot.sound. The post declares that the formalization and the comment were prepared with assistance from Codex 5.5 using xhigh reasoning and ChatGPT 5.5 Pro, the systems as the post names them. A reader replied the same day that a screening check found the Lean correct and described the projection argument. The corpus has not built or audited the development, so it is not formalized evidence. The site's commentary, last edited 29 April 2026, does not record the bound.

Depends on. No page of this wiki.