---

Claim. Kenta Kitamura's Lean development, announced in the discussion thread of Problem 879 on 6 September 2026 and submitted to formal-conjectures as pull request 5302, proves that there is an $n_0$ such that for every $n\ge n_0$ every element of every admissible set attaining $G(n)$ has at most two distinct prime factors (the statement EventualOmegaAtMostTwo). Its target theorem, erdos_879.parts.ii_false, deduces that the second question has answer no: at $k=3$, no optimal set for large $n$ contains an integer with three distinct prime factors. The repository's explanation describes the proof as two exchange arguments, which replace an element with two small prime factors, or with one small and two large prime factors, by elements of larger total sum, with the prime number theorem supplying unused primes in fixed-ratio intervals. The post and the repository state that the development was made with the help of OpenAI Codex and ChatGPT Astra.

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

I have posted a Lean formalization and proof concerning the second part of Erdős Problem 879 to Formal Conjectures: “Is it true that, for every k ≥ 2, if n is sufficiently large, an admissible set which maximises G(n) contains at least one integer with at least k distinct prime factors?”

FC: Formal Conjectures PR #5302 GitHub: erdos-879-lean Lean4Web: standalone Lean4Web proof

The Lean proof gives a negative answer by disproving the statement for k = 3.

AI disclosure: This formalization and repository packaging were developed with assistance from OpenAI Codex and ChatGPT Astra.

Covers. The second question, answered no at $k=3$, and hence for every $k\ge3$. It reads "prime factors" as distinct prime factors, the reading the problem page's Formulation records. The first question, $G(n)>H(n)-n^{1+o(1)}$, is formalized in the repository but not proved.

Standing. Claimed. Pull request 5302 was open on 2026-10-07. The repository reports that #print axioms lists only propext, Classical.choice and Quot.sound, but this corpus has not built or audited the development, so it gives no formalized evidence. The site's label is OPEN.

Depends on. No page of this wiki.