---

Submission note. Posted to the site's forum by Sara Logsdon on 17 August 2026:

Although this is superseded asymptotically by Shouqiao Wang’s subsequent proposed proof that $f(N)=o(N)$, I found that the elementary lattice argument above can itself be refined from $5/6$ to $813/1000.$ I formalized this refinement completely in Lean: Lean repository. The completed asymptotic result appears in the final Lean theorem. This may be of some independent interest as an explicit quantitative strengthening of the elementary argument.

The idea is to refine the decomposition to

$$n=m2^i3^j5^k,\qquad (m,30)=1. >$$

For fixed $m$ and $k$, the selected integers again form a $\Gamma$-free

subset of

$$D(T)=\{(i,j):2^i3^j\le T\},$$

with the usual projection bound

$$> L(T)=\lfloor\log_2T\rfloor+\lfloor\log_3T\rfloor+1.$$

The improvement comes

from the fact that adjacent 5-adic slices cannot attain these bounds independently.

More precisely, suppose an upper slice $F\subseteq D(S)$ is extremal, so $|F|=L(S)$. Then every nontrivial $2,3$-smooth integer $c\le S$ is forbidden in the slice immediately below it. Indeed, $1\in F.$ If $c\in F$, then

$$> \{5,5c,c\}$$

has equal pairwise LCMs. If $c\notin F$, maximality implies that

adding $c$ creates a corner with some $u,v\in F$, and then

$$\{5u,5v,c\}$$

has

equal pairwise LCMs.

Thus the lower slice is forced into

$$\{1\}\cup R(T),\qquad > R(T)=\{2^i3^j:T/5<2^i3^j\le T\}.$$

If $h(T)$ is the largest size of a

$\Gamma$-free subset of $R(T)$, the needed annulus estimate is

$$h(T)\le > L(T)-3\qquad(T\ge120).$$

For large $T$, this follows from a row-counting

argument. The remaining finite range is handled exactly.

Writing

$$d_k=L(T_k)-|F_k|$$

for the deficit in the $k$-th 5-adic slice, this

gives

$$T_k\ge120,\quad d_{k+1}=0 \quad\Longrightarrow\quad d_k\ge2.$$

There

is also the finite two-slice strengthening

$$d_k+d_{k+1}\ge2$$

when

$$45\le > T_k\le71 \qquad\text{or}\qquad 80\le T_k\le119.$$

The finite verification

reduces to the ten states

$$45,48,54,60,64,80,81,90,96,108.$$

These states are

proved inside Lean and were also checked independently by two exact Python programs: one directly enumerates the relevant $\Gamma$-free families, while the other constructs the complete two-layer LCM hypergraph and computes its exact minimum hitting set.

Summing the forced deficits over the 5-adic tower gives total weighted deficit

$$\frac{61}{800}.$$

The cores coprime to $30$ have density $4/15$, so

the saving from the original $5/6$ coefficient is

$$> \frac4{15}\frac{61}{800}=\frac{61}{3000}.$$

Therefore

$$> \frac56-\frac{61}{3000} =\frac{813}{1000},$$

giving

$$> \boxed{f(N)\le(813/1000+o(1))N}.$$

The repository’s GitHub Actions build the

complete Lean proof. I would still greatly appreciate independent mathematical and Lean review.

AI disclosure: the mathematical exploration, verification code, write-up, and Lean formalization were prepared with substantial assistance from ChatGPT/Codex.

The claim. For every $\varepsilon>0$ there is $N_0$ such that every $A\subseteq\{1,\ldots,N\}$, $N\ge N_0$, with no three distinct elements of pairwise the same least common multiple has $|A|/N\le813/1000+\varepsilon$; that is, $f(N)\le(813/1000+o(1))N$ for the function of Problem 536. The repository's final theorem is Erdos536813.eventually_cardinality_ratio_le_813_1000. The argument refines the $5/6$ lattice bound of Kitamura's development through the $5$-adic slices $n=m2^i3^j5^k$ with $(m,30)=1$: an extremal upper slice forces a deficit in the slice below it, a finite check of ten states (done in Lean and by two exact programs) covers the small cases, and summing the forced deficits saves $61/3000$ from $5/6$.

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

Claimant and postings. Sara Logsdon posted the development in the site's thread on 17 August 2026, reporting that the repository's continuous integration builds the complete Lean proof and asking for independent review. The post declares that the mathematical exploration, the verification code, the write-up and the Lean formalization were prepared with substantial assistance from ChatGPT/Codex, the systems as the post names them. 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. Kitamura's 5/6 bound, whose lattice argument the refinement starts from.