---

Claim. Kenta Kitamura posted in the discussion thread of Problem 878 on 2026-09-13, and the same day on the formal-conjectures tracking issue (the two discussion links), a Lean 4 development that answers the first two questions yes. The theorem erdos_878.parts.i (the first formalization link) states that some set of natural density one carries $f(n)=o(n\log\log n)$ and $n\log\log n=O(F(n))$ along it; the theorem erdos_878.parts.ii (the second) states that $\max_{n\le x}f(n)$ divided by $x\log x/\log\log x$ tends to $1$ as $x\to\infty$. Both are closed with answer(True). The post discloses assistance from OpenAI Codex, Astra and ChatGPT; the repository's README names OpenAI Codex and ChatGPT Astra. No informal author is named; Kitamura submitted the development.

The development defines $F(n)$ as the largest sum of a set of distinct, pairwise coprime integers from $2$ to $n$ whose prime factors divide $n$, with no limit on their number, which is the problem page's Formulation. If the number of summands were tied to $\omega(n)$, then $F=f$ and the first question would fail. The repository also checks in Lean that the two maxima differ at $x=210$, a fact it credits to earlier work, and it claims proofs of the site's remark that $F(n)\sim\frac12 n\log\log n$ for almost all $n$ and of Erdős's formula (17) in [Er84e].

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

I have submitted to Formal Conjectures Lean-verified proofs for the following statements:

1. The first question: for almost all $n$, $f(n)=o(n\log\log n)$ and $F(n)\gg n\log\log n$.

2. The second question: $\max_{n\leq x} f(n)\sim x\log x/\log\log x$ as $x\to\infty$.

3. The variant question stated on this forum page: for almost all $n$, $F(n)\sim \frac{1}{2}n\log\log n$.

4. Formula (17) in the original paper [Er84e], which Erdős conjectured but did not prove: if $h(x)=\max_{n\leq x}\omega(n)$ and $m(x)=\max_{n\leq x}f(n)$, then $(xh(x)-m(x))/x\to\infty$.

The Lean formalization was prepared by Kenta Kitamura (KitaKen1).

GitHub: https://github.com/KitaKen1/erdos-878-lean Formal Conjectures submission: https://github.com/google-deepmind/formal-conjectures/issues/997#issuecomment-5651866467

Lean4Web: First question: open the standalone proof Second question: open the standalone proof Sharp $1/2$ variant: open the standalone proof Original formula (17): open the standalone proof

Verification: no 'sorry', 'admit', or project-specific mathematical axioms in the four proof targets; '#print axioms' reports only 'propext', 'Classical.choice', and 'Quot.sound'.

AI Usage Disclosure: This formalization was developed with assistance from OpenAI Codex, Astra, and ChatGPT under my direction.

Covers. The first question (both halves) and the second. Not covered: the third question for all large $x$, the fourth and fifth questions, and the sixth.

Standing. Claimed. The post reports no sorry or admit, and #print axioms reports only propext, Classical.choice and Quot.sound. The corpus has not built or audited the development, no reviewer has assessed it, and the site labels the problem OPEN.

Depends on. Nothing in this wiki.