(git-record date, not publication date)
completed
ordinary mathematical derivation
tooling/method work
verified
The moment-method route to Erdos-Kac costs roughly 2400 to 3700 lines of Lean and every obligation is a thing somebody knows how to write down, while the characteristic-function route is blocked on the fundamental lemma of sieve theory, which Mathlib lacks and which has no Lean formalization.
hunts/r_8c3b94 (Record 36 of 98 in chronological sequence)
Guiding Question
What does each of the two standard routes to a formal Erdős–Kac cost in Lean, given Mathlib at mathlib4 rev 51e6992e (toolchain v4.33.0-rc2) and this tree's zero-sorry base?
Method & Verification
Every Mathlib claim was resolved by compiling Probe.lean against the pin, 43 declarations plus nine from this tree, with misses searched by name over the pinned source rather than remembered.
Lineage & Relationships
Primary Sources (at pin 8fa46e134)
Editorial Notes
Case-log status is settled, a mapping run, not a proving run. Disposition maps settled to completed. Role is tooling/method work because the run priced two routes and walked neither. HuntSpec en-dash in Erdos-Kac is retained in the question; the headline uses ASCII Erdos-Kac.
Date Provenance
commit 22f4be9963aa5828958570674f7c8f4bc5abcad4, hunts/r_8c3b94/RESULTS.md, author 2026-08-18T03:47:34Z