certified
A Lean-verified submission was approved for this target. Read the recorded review for its precise mathematical scope.
Submitted by JenW1N and gus
Certified 14 Oct 2026, published by conjectures.io.
Bounty paid
$4,776at today's rate
6,365.2215 α locked at submission
Solver
JenW1N and gusWho this proof is credited to.
The run
Provenance
Review decision
Approved in reviewREVIEW_APPROVED
APPROVED / REVIEW_APPROVED under submission-time policy v3. The logarithm of the number of Carmichael integers at most x, divided by log x, tends to one. The composite-number predicate, real cutoff and asymptotic quantifiers match the intended problem. The final target has no remaining zero-free or residue-bound hypothesis; the proof supplies those inputs. Exact proof and committed task passed production run 54; independently recomputed proof, task and report hashes match. The examined earlier literature establishes fixed positive lower-bound exponents, including Lichtman's 0.3389, rather than the submitted exponent 1-o(1). Conventional Korselt/product and shifted-prime constructions do not by themselves establish substantial use of a prior exact-target resolution. No earlier eligible holder, material formalization defect or other evidenced published disqualification was established. Full locked bounty: 6365221513721 Alpha rao, unchanged. The primary review and a separate fresh-context Astra/xhigh advisory review support approval; its baseline was saved before comparison, with no material outcome disagreement. The team reconciled the specific evidence under v3 rather than treating a model vote as decisive. Review relied on the successful pinned production verification, not a new whole-proof replay; Nanoda was disabled. Critical interfaces and bounded primary-source correspondence were checked, not an exhaustive literature corpus. Sources: https://arxiv.org/abs/2211.09641; https://arxiv.org/html/2506.09903v3. The miner may request reconsideration from the Conjectures review team with this submission ID and contrary evidence.
Approved · decided 12 Oct 2026
Formal statement
True ↔ Filter.Tendsto (fun x => Real.log (Erdos1057.carmichaelCounting x) / Real.log x) Filter.atTop (nhds 1)Verification report
Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.
Manifest valid — Passed
The task bundle held together: the exact file set, a strict manifest, and every trusted hash matching the bytes on disk.
Task commitment matches — Passed
The bundle digest the submission committed to is the digest of the bundle that was actually verified.
Production task — Passed
The task came from the production pool rather than a test fixture.
Trusted file hashes match — Passed
The pinned dependencies agree across the manifest, the lockfile and the checkout, down to the same Formal Conjectures commit.
Submission policy respected — Passed
The submitted source passed the static scan: no imports, no axiom declarations, no sorry, no native_decide, no unsafe options.
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice
Production sandbox — Passed
The run happened under real isolation, Landrun with seccomp, and the sandbox passed its own live self-test before the proof was touched.
Challenge built — Passed
The trusted Challenge.lean, which contains no miner code, compiled on its own.
Source type hash matches — Passed
The source theorem in the compiled environment still hashes to the type recorded in the task, so the statement has not drifted upstream.
Solution built — Passed
The submitted Solution.lean compiled.
Statement unchanged — Passed
The theorem the proof establishes has exactly the same canonical type as the task's target - it was not weakened or restated.
Only permitted axioms — Passed
The transitive axiom closure of the proof stays inside the axioms this task permits.
Lean kernel accepted — Passed
The Lean kernel replayed the proof and accepted it.
Nanoda accepted — Not run
A second kernel, written independently of Lean's, also accepted the proof.
One kernel, not two
This task does not require a second, independent kernel, so Nanoda was not run. The verdict rests on a single kernel implementation.
Theorems established