---

Claim. For every nondecreasing $f:\mathbb N\to\mathbb R$ with $f(n)\to\infty$ and $f(n)\le\log n$ eventually, the values

$$F(f,n)=\frac{\tau((n+\lfloor f(n)\rfloor)!)}{\tau(n!)}$$

with $n\ge N$ are dense in $(1,\infty)$ for every $N$. Taking $f(n)=\log n$ answers the second question as well. Plasma AI's formalization proves the two statements as Erdos420.erdos_420.parts.iii and Erdos420.erdos_420.parts.ii.

Covers. The parts logarithmic_density and monotone_density of Problem 420. The first question, part divergence, asking whether $F((\log n)^C,n)\to\infty$ for large $C$, is not covered.

Formalization. The version retained on the source card pins Lean and Mathlib v4.35.0-rc4. Its proof derives a uniform power-saving prime-number theorem in arithmetic progressions from a vendored Lean proof of the Dirichlet seven-eighths zero-free theorem, combines a protected CRT covering with Maynard's sieve and a Selberg upper-sieve tail bound, and concludes by sliding the factorial window. The zero-free theorem is a proved dependency, not a hypothesis of the final statements. formalization.yaml credits Jacob Parish as the formalization's author and records assistance from Claude Code, model claude-opus-5-5.

Acceptance. Accepted on 2026-10-20 on the formalization. The independent reproduction rebuilt every Problem 420 module in a fresh source tree, using checked caches for the vendored dependencies. Comparator accepted both targets. Separate empty-environment kernel replays checked their complete proof closures, with no unsafe or partial declarations and only propext, Classical.choice and Quot.sound; both target types and all their statement dependencies matched the challenge.

The independent statement-fidelity review found both statements faithful to the two density questions, and a distinct fresh-context grader gave PASS. The grader ruled the disclosed general-instruction exposure immaterial. This acceptance covers the two density questions and assigns no native claim tier.

Depends on. The formalized density theorem, whose dependency closure includes the Dirichlet seven-eighths zero-free theorem.