Lean

Erdős Problem 357: bounds on sequences with distinct consecutive sums, formalized in Lean

For Erdős Problem 357, the largest k with 1 ≤ a₁ < … < aₖ ≤ n and all consecutive sums distinct satisfies f(n) ≤ (44273/90000)n + 2√n + 177792 and, for large n, f(n) ≥ (15/√21)√n − 1800. The proofs and the Lean formalization were produced by AI agents, and the Lean statements are pinned to the community’s formal definition. Whether f(n) = o(n) is still open.