---

Claim. For $p=2$ and every $1\le a\le256$ the exponents $k$ with $2^k\mid a_1!+\cdots+a_n!$ for some $a=a_1<\cdots<a_n$ are bounded, the first question of Problem 404 at these pairs, and the largest such exponent $f(a,2)$ is computed exactly; in particular $f(2,2)=254$, the value of Lin's upper bound on his page, and the largest value in the range is $f(34,2)=18444$. Kenta Kitamura, under the forum name KentaKitamura, announced the repository KitaKen1/erdos-404-p2-landscape in the site's discussion thread on 7 July 2026; its README (linked at the commit of that day, data status 6 July 2026) is the write-up. Each value is certified from both sides: an explicit increasing list whose factorial sum is divisible by $2^{f(a,2)}$, and an exhaustive search showing that no list reaches $2^{f(a,2)+1}$. The search is finite because, by Legendre's formula, $v_2(n!)\ge K+1$ for all $n$ beyond a point, after which every factorial vanishes modulo $2^{K+1}$; the candidate terms are therefore bounded, and a dynamic program over the reachable residues of partial sums modulo $2^{K+1}$ decides whether $0$ is reached. For odd $a$ the value freezes at $f(a,2)=v_2(a!)$, since every later factorial is divisible by a higher power of $2$ than $a!$; for even $a$ the values vary widely. Three values carry Lean 4 certificates: the file S404_lean4web_2_2.lean (the formalization link) proves $f(2,2)=254$ from both sides, the lower bound from the $119$-term witness and the upper bound by running the finite search inside the kernel with decide, in core Lean without Mathlib and, as its header says, with no axiom beyond propext; companion files prove $f(4,2)=6$ and $f(5,2)=3$. This corpus has not built them, so they give no formalized evidence. The post and the README say the repository, the Lean files and the post were prepared with assistance from Codex 5.5 (xhigh reasoning), ChatGPT 5.5 Pro and Claude Code (Fable 5); the human submitter is the claimant, with the systems named as the submitter names them.

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

I made an attempt repository for exact values in the $p=2$ column of Problem #404: $f(a,2)\quad(1\le a\le256).$ Repository: https://github.com/KitaKen1/erdos-404-p2-landscape Visual table: https://kitaken1.github.io/erdos-404-p2-landscape/

In particular: $f(2,2)=254.$ This is worth singling out because the Problem #404 page records Lin's upper bound $f(2,2)\le254$; the repository gives the matching lower-bound witness and a two-sided Lean/lean4web check. Lean4web for $f(2,2)=254$: https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2FKitaKen1%2Ferdos-404-p2-landscape%2Fmain%2Flean%2FS404_lean4web_2_2.lean

Here $v_2(m)$ denotes the exponent of $2$ in $m$. The lower-bound side is just an explicit increasing list whose factorial sum is divisible by the claimed power of $2$. The upper-bound side is finite: by Legendre's formula,$v_2(n!)=\lfloor n/2\rfloor+\lfloor n/4\rfloor+\lfloor n/8\rfloor+\cdots,$ so to rule out exponent $K+1$, search modulo $2^{K+1}$, and once $v_2(n!)\ge K+1$, all later factorials are $0$ modulo $2^{K+1}$.

For odd $a$, this immediately freezes the value at $f(a,2)=v_2(a!)$. For even $a$, cancellations make the values much wilder.

The repository also records a few observations from the table. For example, the largest value found in $1\le a\le256$ is $f(34,2)=18444.$

AI usage: the repository, Lean files, and this comment were prepared with assistance from Codex 5.5 (xhigh reasoning), ChatGPT 5.5 Pro, and Claude Code (Fable 5).

Covers. The first question for $p=2$ and each $1\le a\le256$: a finite bound exists, with $f(a,2)$ computed exactly, for example $f(2,2)=254$, $f(4,2)=6$, $f(5,2)=3$ and $f(34,2)=18444$. Not covered: $a>256$, odd primes (the odd-prime rows are on the companion page), the behavior of $f$ in general, and the third question.

Depends on. No page of this wiki.

Standing. Claimed: a research note in a public repository, unrefereed, not cited by the site's commentary, with Lean certificates this corpus has not built; the site labels the problem OPEN. The claim stays claimed.