Mathematics

Specific problems and progress on them.

1. QL-0023

   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.

   Investigation MA.1 Reproduced
   2026-10-23Rev. A

Proof assistants and machine-checked mathematics.

No entries in this section yet.