What was already known
The problem catalog asked for all positive exponents. Pratt proved the k=4 case and described earlier partial results; the project’s all-exponent proof is presented as an original development rather than a formalization of a published general proof.
AI involvement
Tokengrinder directed the target, proof obligations, reviews and publication. The Palomar account says Codex and Claude agents supplied substantive mathematical proof construction and Lean work; finer per-agent attribution was not consistently recorded.
Tokengrinder directed the target, obligations and review. The project account credits Codex and Claude agents with substantive all-exponent proof construction as well as Lean development, without reliable finer per-agent attribution.
Importance
Gives one proof of the full exponent family in a named Erdős problem, beyond the previously cited special cases.
Limitations
The source warns its literature search is not exhaustive and does not claim transcendence or relations among different sums. It reports a completed local Lean proof and statement audit, but no independent human expert review; Palomar registration status is separate.
Technical verification
The source reports full build, trust-zero rebuild, statement and axiom audits, and fresh kernel replay of the all-exponent theorem. This applies to the selected claim and is not an independent reproduction by AIProofWatch.
Formal checking
The source reports a source-only Lean proof with no holes, a trust-level-zero statement audit, standard-axiom check and fresh leanchecker replay. The Challenge placeholder is not imported into Solution.
- Checker
- Lean 4 kernel and documented local statement, axiom or certificate audits run by repository authors
- Scope
- For every natural k≥0, the convergent series Σₙ≥1 σₖ(n)/n! is irrational, where σₖ(n) is the sum of kth powers of positive divisors of n. The k>0 cases answer Erdős Problem 252; the Lean theorem also handles k=0.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The project reports agent review and the human author’s direction but no independent human expert review or human explanation of the full proof mechanism. Few is the evidence default.
Correction and publication history
Claim-level primary-source review of exact theorem, prior baseline, AI contribution and documented checking scope.
Read this published revision