Lean-verified proofs for [42]

Sergeev I. S. On the additive complexity of some integer sequences. Mathematical Notes. 2024. 115(3), 378-389.

Complexity of 0-chains for 2ⁿ–1 (Theorem 2 and corollaries). LEAN

Lower bound for B_k-sets (Theorem 4). LEAN

Corollary for the complexity of the set H[n, k]. LEAN (requires Theorem 4)

An example of easy-to-compute sum-free Sidon set (Theorem 5). LEAN

Lean-verified proofs were derived by an AI-assistant from text proofs in Reaslab environment.