---

Claim. The answer to Problem 646 is yes. Berend proves that for every $k$ there are infinitely many positive integers $n$ such that each of the first $k$ primes appears to an even exponent in the prime factorization of $n!$; the paper's abstract presents this as the answer to the question of Erdős and Graham. Any finite set of distinct primes $p_1,\ldots,p_k$ lies among the first $K$ primes for some $K$, so the theorem gives infinitely many $n$ with $n!$ divisible by an even power of each $p_i$, which is the question in the reading the problem page's Formulation records. The site's commentary adds that the paper proves more: the integers $n$ with this property have bounded gaps, the bound depending on the primes. The paper is not held; the statement is taken from the paper's abstract, the site's problem page and the docstring of the Lean file below, to whose author the paper's text up to the end of the proof of its Theorem 1 was available.

Depends on. No page of this wiki; the result rests on the cited paper.

Formalization. The Lean file Erdos646.lean in Boris Alexeev's repository of Lean proofs declares itself a formalization of a solution to the problem, with Berend as its informal author and the AI system Aristotle (Harmonic) and the forum user JoshuaB as its formal authors; its header says Aristotle generated the file. JoshuaB announced the formalization in a thread post of 2026-02-27 that linked Lean web-editor sessions holding it; Alexeev's repository took in a copy on 2026-05-06, and the link above is the later revision of 2026-06-30 that the formal-conjectures record names. The post says its author gave Aristotle the text of Berend's paper up to the end of the proof of Theorem 1 and asked it to prove the problem statement, that Gemini 3.0 Flash wrote a readable statement of the result, and that the Lean lemmas differ in detail from Berend's Lemmas 2 and 3; an edit to the post adds that its main theorem differs from Berend's Theorem 1 as well. Its theorem infinitely_many_even_factorial_exponents states that for $k$ distinct primes $p_1,\ldots,p_k$ the set of $n$ for which every exponent of a $p_i$ in $n!$ is even is infinite, the question as the site states it; the bounded gaps are not formalized. The formal-conjectures record tags erdos_646 solved and names this file at that revision as its formal proof; the file at that revision contains no sorry. This corpus has not built or audited the file, so the page lists no formalized evidence.

Acceptance. The site's curator, T. F. Bloom, marks the problem proved and credits this paper, which the page lists as reviewed. The paper is D. Berend, On the parity of exponents in the factorization of $n!$, J. Number Theory 64 (1997), no. 1, 13--19, a refereed journal, listed as refereed. The page is dated by the publisher's record, which gives May 1997 for the issue; the first day of that month stands in for the issue date.