{"id":"palomar/PALOMAR-2026-10-15-000013","url":"https://github.com/AxiomMath/CollatzPositiveDensity/tree/3a38bfbb70379e051b51155def1423846fab3a90","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000013-v1.json","repo":"https://github.com/AxiomMath/CollatzPositiveDensity","tags":["math.NT","msc:11B83","msc:37P99","msc:60G50","collatz-conjecture","density-estimates","formal-verification"],"score":0,"title":"CollatzPosDens","trust":"high","domain":"math.NT","source":"palomar","authors":["Kenny Lau"],"reviews":0,"subject":"math.NT","summary":"`CollatzPosDens` is a formal proof of the main results of *Explicit positive lower density for the Collatz Conjecture* (hexagon:2610.00249). It proves Theorem 1.3, an explicit positive density of odd starting values reaching a prescribed target $t$ with $3 \\nmid t$; Remark 1.4, which replaces the odd part of $t$ by $t$ itself when $\\gcd(t, 6) = 1$; and Corollary 1.2, the case $t = 1$. The Lean files were generated by AxiomProver, Axiom Math's in-house theorem proving system.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-15","reactions":{},"formalized":true,"formalizes":[{"title":"Explicit positive lower density for the Collatz Conjecture","identifier":"https://hexagonmath.org/2610.00249","relationship":"formalizes"}]}