Conjecture 4.6 for truncations of the ring of number-theoretic functions
The generator counts satisfy , which proves the six-part reduced Poincaré--Betti-series conjecture and yields new exact and asymptotic consequences.
Details and sources
AI contribution
Snellman reports that Claude found the counting identity, the reduction and proof of Conjecture 4.6, further asymptotics and errata, wrote the SageMath and Lean code, and drafted the manuscript under his direction.
Problem origin
Jan Snellman posed Conjecture 4.6 in his human-authored 2000 paper, supported by computations through .
Verification
Author-checked proof, independent computations, partial Lean coverage
Claim audit
Lean covers the polynomial argument and four of the six clauses of the conjecture, not the entire paper. This audit inspected the public scope statement but did not rebuild the GitLab project.
Publication
Public arXiv paper with SageMath and Lean companion artifacts
Preprint / manuscript
The paper also corrects one false statement and two incomplete proofs in the 2000 source. The Lean artifact is substantial but should not be read as an end-to-end formalization of every analytic result.
- Claimed outcome
- Proved
- Problem origin
- Human-source problem
- System
- Claude (version undisclosed)
- Verification
- Author-checked proof, independent computations, partial Lean coverage
- Claim audit
- Issue documented