---

Claim. The answer to Problem 1057 is yes: if $C(x)$ counts the Carmichael numbers in $[1,x]$, then

$$\frac{\log C(x)}{\log x}\to1\qquad(x\to\infty),$$

that is, $C(x)=x^{1-o(1)}$. The proof is a Lean 4 file of 393,097 lines (about 17.7 MB) with no import statement, submitted under the handle JenW1N to the bounty site Conjectures.io, which had published the problem as the formal-conjectures declaration Erdos1057.erdos_1057 with its answer left open. The file's final theorem, Bounty.target, takes the type of that declaration with the answer True and is closed by WeakZeroFree.target_of_selected_residue_bounds applied to the proved candidate_selected_residue_bounds, with no hypothesis left. Read from the statements of its main declarations, the route is that of Alford, Granville and Pomerance [AGP94]: Carmichael numbers are built as products of primes $p$ from a set whose predecessors $p-1$ are smooth, a count of such products gives $C(x)\ge x^{1-\varepsilon}$ for every fixed $\varepsilon>0$ and all large $x$ (NearLinearLowerBound), and the limit follows with the trivial $C(x)\le x$ (target_of_lower_bound). Its two analytic inputs are a zero-free half-plane $\operatorname{Re}s>23/24$ for every primitive nonprincipal Dirichlet $L$-function (WeakZeroFree.actual_zero_free), which it turns into the bound $\psi(x,\chi)\ll x^{95/96}\log(qx)$ for the prime sum twisted by a primitive character $\chi$ of modulus $q$ (WeakZeroFree.primitive_twistedPsi_power_saving), and a supply of primes with smooth predecessors, which a large part of the file's own modules prove by moment and Fourier estimates. A comment block left in the file from an earlier stage calls it an incomplete formalization whose smooth-prime and zero-free inputs are unproved; the final declaration takes neither as a hypothesis. No write-up accompanies the proof, and the file names no author for it and declares no AI system. The handle is Liam Kruer and Jensen Kohlmeyer's: the bounty site's exposition of their JenW1N record on Problem 196 names them as its authors, and Kruer's post of 5 October 2026 on erdosproblems.com, announcing their Lean formalization of a Problem 790 claim in the GitHub account JENW1N, is signed "(Jensen Kohlmeyer and Liam Kruer)".

The formal statement. The task is the formal-conjectures declaration Erdos1057.erdos_1057 (FormalConjectures/ErdosProblems/1057.lean at the formal-conjectures commit of 2026-09-18, the file's last change) with its open answer fixed to true: the limit of Real.log (carmichaelCounting x) / Real.log x as the real $x$ tends to infinity is $1$. There carmichaelCounting x is the number of natural numbers $n\le x$ with IsCarmichael n, and IsCarmichael n (FormalConjecturesForMathlib/NumberTheory/Carmichael.lean at the same commit) says that $n$ is a Fermat pseudoprime to every base $b\ge1$ coprime to $n$, that is, $n>1$ is composite and $n\mid b^{n-1}-1$ for all such $b$, the usual definition. Since $1\le C(x)\le x$ for $x\ge561$, the limit $\log C(x)/\log x\to1$ is exactly $C(x)=x^{1-o(1)}$, and the answer true is the affirmative answer. So the formal target is the problem's question with the same quantity, limit and polarity. Conjectures.io's record prints the target with the answer True. The task pins a catalog commit that Conjectures.io builds from a public catalog commit and an audit patch, which changes 1057.lean only by writing IsCarmichael as _root_.IsCarmichael; this corpus's replay reproduced that commit exactly and found the target's type identical to its statement.

The zero-free input. WeakZeroFree.actual_zero_free is derived from OAI.ApplicationAudit.nonprincipal_LFunction_ne_zero, in a module of the file marked PinnedNonprincipal, which is not a module of the OpenAI release. That theorem states that $L(s,\chi)\ne0$ for every nonprincipal Dirichlet character $\chi$ and every $s$ with $\operatorname{Re}s>23/24$. Its proof applies lemmas of the release's inlined modules directly, among them the fixed-shell models actual_fixedShellModels of OAI.NumberTheory.DirichletL.RowCompletion.ZeroFreeRegion. The file's copy of that module keeps CanonicalRowCompletion.dirichletTarget_unconditional, that no Dirichlet $L$-function vanishes in $\operatorname{Re}s>23/24$ apart from the pole at $s=1$, but omits the release's theorem ShortDraft.dirichlet_LFunction_ne_zero. The inlined tree is the release's formalization of its zero-free half-plane work, whose stronger claimed half-plane $\operatorname{Re}s>7/8$ is [[../library/primes/openai_2026_quasi_riemann_hypothesis_zero_free_half_plane_7_8/theorem_1_1|Theorem 1.1 of The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s)>7/8]]. The file uses only the weaker half-plane $\operatorname{Re}s>23/24$, names that seven-eighths proof as the source of a few extracted numerical lemmas, and does not inline its main theorem.

Depends on. No page of this wiki is a premise: the file proves its inputs in Lean. It inlines external Lean code, each piece marked by its source module or a port note. The largest part is 286 modules OAI.NumberTheory.DirichletL.* of the openai/math Lean release (Apache-2.0, its first commit, of 6 October 2026). With that tree come 15 modules of Adam Benenson's Lean proof of the Rellich--Kondrachov theorem (Apache-2.0, "Authors: Adam Benenson"), a dependency the release's lakefile pins. The file also ports 12 modules OAI.NumberTheory.Ostmann.* from the same release commit (a zero-count argument for Dirichlet $L$-functions), and modules of the PrimeNumberTheoremAnd project (Apache-2.0): complex-analysis auxiliaries carrying Michael Stoll's copyright and elementary Mertens estimates.

Acceptance. Formalized. This corpus's verification rebuilt the record's solution file, unchanged, on the repository's pinned toolchain, leanprover/lean4:v4.34.1 with Mathlib at the revision lean/lake-manifest.json pins. The kernel replayed, from an empty environment, every declaration the target Bounty.target depends on, Lean core, Mathlib, formal-conjectures and the inlined modules included, and accepted them all. The target's axioms are exactly propext, Classical.choice and Quot.sound. Its type, and every definition its statement reaches, are identical to the formal-conjectures statement of Conjectures.io's task, which The formal statement. above reads as the problem's question, with IsCarmichael the usual definition. Acceptance rests on this replay and that check.

The bounty site's approval is reported, not counted. Conjectures.io's Lean kernel verified the file against its task on 10 October 2026 (20:43 UTC), with the axioms propext, Quot.sound and Classical.choice permitted and no second kernel run, and its review approved the record on 12 October 2026 under its policy v3. The review record says that the formal statement matches the intended problem, that the final target keeps no zero-free or residue-bound hypothesis, that a primary review and a separate fresh-context advisory review supported approval, and that the review relied on Conjectures.io's production verification without a new whole-proof replay. The record was not certified when read on 13 October 2026: it showed the Lean verification passed, the review approved and the reward eligible, with the bounty pending and no certification date. No refereed publication or review outside the bounty site exists. The corpus also read the file as text: its header, its final declarations and the chain from Bounty.target to the zero-free input were checked against Conjectures.io's statement, and a text scan found no sorry, axiom declaration, native_decide, implemented_by, unsafe, set_option or import. Bloom's catalog labeled the problem OPEN, and the proof has no entry on its proof-claims tab, which was frozen on 6 October 2026, before the submission.

Replay record. The receipt of the kernel replay.