---

Claim. On 2026-05-02 Lech Mazur posted in the thread of Problem 1194 a lower bound that, in Mazur's words, GPT-5.5 Pro, Codex and a verification harness found; the full write-up names GPT-5.5 Pro and Mazur as its authors. Here $a_n$ is the larger member of the unique representation $n=a_n-b_n$. With $\lambda=1/(2\log2)$ and $B_1=\tfrac12+\gamma-\log\log2$, for every fixed $B>B_1$ infinitely many $n$ satisfy $a_n>\lambda n^2/(\log n-\log\log n+B)$. Consequently $\limsup_{n\to\infty}a_n(\log n-\log\log n+B_1)/n^2\ge\lambda$; the endpoint $B=B_1$ is claimed only in this limsup form. The full proof and a sketch are PDFs in the claimant's repository, which also holds a Lean development whose Challenge.lean states the two results as FloorSaving.floor_saving_lower_bound and FloorSaving.endpoint_limsup.

Submission note. Posted to the site's forum by Lech Mazur on 2 May 2026:

GPT-5.5 Pro + Codex + a verification harness found the following improvement.

Let

$$\lambda=\frac{1}{2\log 2}, \qquad B_1=\frac12+\gamma-\log(\log 2).$$

For

every fixed $B>B_1$, infinitely many $n$ satisfy

$$a_n> \lambda\frac{n^2}{\log > n-\log\log n+B}.$$

Consequently,

$$\limsup_{n\to\infty} \frac{a_n(\log > n-\log\log n+B_1)}{n^2} \ge \lambda = \frac{1}{2\log 2}.$$

The endpoint

$B=B_1$ is only claimed in this limsup form, not as a pointwise infinitely-often inequality.

Lean repository: https://github.com/lechmazur/erdos_1194

Proof sketch: floor_saving_proof_sketch.pdf

Full proof: floor_saving_lower_bound_final_version.pdf

Covers. A lower bound of order $n^2/\log n$ for $a_n$ along infinitely many $n$. It does not determine how fast $a_n/n$ must grow.

Standing. A reader's AI check, posted, reported one minor issue in the write-up, noted that the write-up's length made the check less reliable, and judged that the Lean appears to formalize the result. This corpus has not built the Lean development or audited its definitions, so the Lean is a link, not formalized evidence. The claim is unrefereed and stays claimed.

Depends on. No page of this wiki.