---

Claim. For a list $A=(n_1,\ldots,n_r)$ of positive moduli, let $D_{\max}(A)$ be the largest density of a union of classes $a_i\pmod{n_i}$, one per modulus, the first question of Problem 278. For a residue choice, call $i$ and $j$ compatible when $\gcd(n_i,n_j)\mid a_i-a_j$, and let $G(a)$ be the graph of compatible pairs. By the Chinese remainder theorem a subfamily $S$ has a common point exactly when $S$ is a clique of $G(a)$, and then its intersection is one class modulo $L_S=\operatorname{lcm}_{i\in S}n_i$, so inclusion-exclusion gives the density $W_A(G(a))=\sum_{\emptyset\ne S\text{ clique}}(-1)^{|S|+1}/L_S$. The manuscript claims

$$D_{\max}(A)=\max_{G\text{ realizable}}W_A(G),$$

the maximum over the graphs $G(a)$ that some residue choice realizes, and that these graphs are exactly the complements of the states reached by a finite dynamic program: it writes the moduli as products of pairwise coprime bases computed by repeated gcd splitting, without factoring, and at each digit coordinate records which pairs are separated by unequal digits. From this it derives a deterministic algorithm computing $D_{\max}(A)$ and attaining residues in $2^{O(r^2)}\operatorname{poly}(B)$ bit operations, $B$ the binary input length, refined to $2^{O(m)}\operatorname{poly}(B)$ with $m$ the number of pairs of moduli sharing a factor, and an exact mixed-integer formulation with $r^2-1$ integer variables. It gives $D_{\max}(2,6,10)=11/15$ as an example. The manuscript, Exact Optimization of Congruence-Class Unions: Fixed-parameter algorithms and a Lean verification (version 1.2, dated 11 September 2026, the PDF linked above), is accompanied by a Lean 4 development of 165 declarations in 26 modules whose principal theorems, Erdos278.verified_maximum_density and Erdos278.verified_dp_maximum_density, are said to prove the graph formula, the model correspondence and the optimality of the dynamic program's value for every nonempty input, with density defined by counting residues of a period; the author reports that every declaration uses only propext, Classical.choice and Quot.sound. The manuscript's appendix discloses that GPT-5.6 Sol and GPT-6 Astra were used for exploration, drafting, Lean development, computation and literature search; the site's claim names both systems. Related work the manuscript cites includes the fixed-parameter pinwheel results of Kobayashi and Lin and the digit representation of Jacobs and Longo.

Submission note. Posted to erdosproblems.com as a proof claim by Onishi Yoshiharu (account Raki) on 10 September 2026, giving "GPT-5.6 Sol and GPT-6 Astra" as the AI used:

I claim a complete solution to the first question of Erdős Problem 278. I prove

$$D_{\max}(A)= \max_{G\text{ realizable}} \sum_{\substack{\emptyset\neq > S\subseteq[r]\\ S\text{ clique in }G}} > \frac{(-1)^{|S|+1}}{\operatorname{lcm}_{i\in S}n_i}$$

and show that a

gcd-based dynamic program characterizes exactly all realizable compatibility graphs. This yields an exact algorithm and attaining residues for every finite set of prescribed positive moduli.

Covers. The first question, as an exact characterization and algorithm for the maximum covered density of any finite set of moduli; the manuscript describes this as an algorithmic treatment and assumes no particular kind of closed formula. The second question is Simpson's (claim page). Whether the characterization answers the question as intended is the point the site's thread leaves open: Cambie's comment of 2026-09-11 on the claim calls it a complementary attempt to Cambie's own hardness arguments (claim page) reaching an essentially opposite answer, defers the thread's closure to the site's curator, and notes that for moduli up to $2^{\varepsilon r}$ the stated bound is not smaller than enumerating all residue tuples; the author's reply agrees that the bound alone is no asymptotic gain in that regime, stresses that for fixed $r$ the optimum is polynomial in $B$ for arbitrary moduli, sees no mathematical contradiction with the NP-hardness results, and asks that the work be judged as a proposed resolution of the minimum-uncovered-density part.

Depends on. Nothing in this wiki.

Standing. Claimed: the manuscript is a release PDF on the author's repository with no journal publication, referee report or curator acceptance located; the site labels the problem OPEN (page last edited 20 January 2026). The releases are dated 2026-09-10 (versions 1.1 and 1.2; the proof claim was submitted the same day), which gives the page its date; the formalization link pins the commit of version 1.2. This corpus has not built or audited the Lean development, so it gives no formalized evidence and is described, not counted.