---

Claim. The case $k=3$ of Problem 979: with $f_3(n)$ the number of multisets of three primes whose cubes sum to $n$, $\limsup_n f_3(n)=\infty$. Kenta Kitamura, publishing on GitHub under the login KitaKen1, published on 17 August 2026 a Lean 4 repository whose main theorem Erdos979.erdos_979.variants.k3 states exactly this, with the counting set copied from the formal-conjectures statement of the variant. The README reports that the proof follows the complex-multiplication route for the Fermat cubic $X^3+Y^3+Z^3=0$: a Hasse bound through cubic Jacobi sums, Hecke angles from primary Eisenstein integers, and the Wiener--Ikehara theorem with the prime number theorem in the progression $1\bmod 3$, taken from the PrimeNumberTheoremAnd library. It reports that the final theorem depends only on the axioms propext, Classical.choice and Quot.sound, and it claims nothing about the cases $k\ge4$ or about the growth rate of $f_3$.

Kitamura announced the proof in the problem's thread the same day, stating that Erdős's method is unknown and that the proof should be regarded as an independent proof, not a reconstruction of Erdős's argument. The README and the post say the formalization was developed with assistance from OpenAI Codex, Fable5 and Claude Code.

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

I have now completed a Lean 4 proof of the k = 3 case.

Repository: https://github.com/KitaKen1/erdos-979-k3

Lean4Web: https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2FKitaKen1%2Ferdos-979-k3%2Frefs%2Fheads%2Fmain%2Flean4web%2FErdos979Lean4WebLatest.lean

The final '#print axioms' reports only 'propext', 'Classical.choice', and 'Quot.sound'; in particular, it does not depend on 'sorryAx'.

Since Erdős's proof was unpublished, his method is unknown. I therefore do not know whether Erdős used anything resembling the approach formalized here. This should be regarded as an independent proof, not a reconstruction of Erdős's argument.

AI usage disclosure: The formalization was developed with assistance from OpenAI Codex, Fable5, and Claude Code.

— Kenta Kitamura (KitaKen1)

Covers. The case $k=3$, with no rate of growth. The cases $k\ge4$ are not touched.

Depends on. No page of this wiki.

Standing. Since 17 August 2026 the formal-conjectures statement file (record link above, pinned at the commit that added it) has named this repository, at the linked commit, as the formal_proof of erdos_979.variants.k3. Commits to the repository after the linked one and up to 2026-10-07 changed only its README. The claim was not filed on the site's proof-claims tab, the site's label is OPEN, no reviewer is named, nothing is refereed, and this corpus has not built the Lean, so the page lists no evidence and the claim stays claimed. The other claims of the case $k=3$ are Erdős's unpublished claim and Wang and Zhang's preprint.