Erdős Problem #870: paper and Lean 4 formalization

Copyright 2026 David Turturean

The Lean source code and repository documentation are licensed under the
Apache License, Version 2.0. See LICENSE for the full text.

The included paper, "Additive bases with many representations and no minimal
subbasis: A negative answer to Erdős Problem #870," is authored by David
Turturean and remains copyright its author.

The construction uses and strengthens ideas from:
Daniel Larsen and Michael Larsen, "Robust additive bases without minimal
subbases," arXiv:2601.18507 (2026).

The natural-language proof was developed with the assistance of GPT-5.4-Pro,
and subsequently GPT-5.5-Pro. The Lean formalization was carried out with the
assistance of GPT-5.5-Pro, Codex (GPT-5.5-xhigh), and Claude Code (Opus 4.8,
maximum thinking). Compute resources were provided by Fulcrum
(https://fulcrum.inc). David Turturean is responsible for the final
mathematical claims and exposition.