Naoki Takata
January 11, 2026
An r-powerful number is a positive integer n such that for every prime p dividing n, we have p^r | n. We study the problem of expressing an r-powerful number as a sum of coprime r-powerful numbers. We formalize in Lean 4 the definitions and key examples, including Nitaj's construction for r = 3 and Cambie's example for r = 5. We verify the Lander–Parkin counterexample to Euler's sum of powers conjecture. We define the Nitaj map and prove that, under certain positivity conditions, it generates infinitely many solutions to the 3-powerful sum problem. All results have been formally verified in the Lean 4 proof assistant using the Mathlib library.
As a proof of existence for this paper, the Keccak-256 hash of the PDF has been recorded on the Ethereum blockchain.
Timestamp: January 11, 2026 (date recorded on the blockchain)
All theorems are formalized in Lean 4 (Mathlib commit f897ebcf72cd16f89ab4577d0c826cd14afaafc7). The verification used Aristotle, an automated theorem proving system for Lean 4.
Naoki Takata
X: @naokitakata
Email: [ntakata [at] proton.me]
This is a preprint. Comments are welcome!