Naoki Takata
January 10, 2026
We study the function g(n), defined as the minimal cardinality of a subset A ⊆ {0, 1, …, n} such that every element of {0, 1, …, n} can be expressed as the sum of two elements of A. We establish an upper bound g(n) ≤ 2√n + 2 using a construction based on the Mrose–Rohrbach method, and a lower bound g(n) ≥ √(2n) − 1 via a counting argument. These bounds confirm that g(n) ∼ 2√n asymptotically. 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 10, 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!