Erdős Problem #870

Additive bases with many representations and no minimal subbasis

David Corneliu Turturean, Fulcrum, davidct@mit.edu

This repository contains the paper and Lean 4 formalization of a negative answer to Erdős Problem #870.

Result

For every integer k >= 3 and every real constant C > 0, there is a set E of positive integers such that:

1. every sufficiently large integer is a sum of at most k elements of E;
2. every sufficiently large n has at least C log n nondecreasing representations using at most k elements of E; and
3. no order-k subbasis of E is minimal.

Thus no constant c(k) can force a minimal subbasis from a logarithmic representation lower bound.

The public Lean declarations are:

Erdos870.main_theorem : Erdos870Target
Erdos870.erdos_870    : Erdos870Target

Start here

• For the mathematics: read paper/erdos_870_paper.pdf.
• For the final theorem: open Erdos870/Main.lean, then Erdos870/MainTheorem.lean.
• For a guided tour: use notes/FORMALIZATION_GUIDE.md and notes/PAPER_TO_LEAN.md.
• For verification details: read notes/AXIOM_AUDIT.md and inspect the GitHub Actions run.

Proof at a glance

The proof has one order-two probabilistic source and two deterministic endings.

• The Larsen-Larsen order-two construction supplies a sparse basis with logarithmically many exact pair representations and a deletable element in every order-two subbasis.
• For k >= 4, a finite residue-class filler gadget reserves two summands for the order-two core, amplifies the representation count, and preserves non-minimality.
• For k = 3, a parity reduction leaves only one filler. A clustered canary construction controls all finite shifts created by that reduction simultaneously.

The formalization expands the probabilistic estimates, finite schedules, exceptional sets, Borel-Cantelli arguments, and interface conversions consumed by the final theorem.

Repository contents

.
├── Erdos870.lean                    # Lean root importing the complete project
├── Erdos870/
│   ├── Main.lean                    # Public theorem `erdos_870`
│   ├── MainTheorem.lean             # Core theorem `main_theorem`
│   ├── Defs.lean                    # Representations, bases, minimality, target
│   ├── Filler.lean                  # Deterministic k >= 4 and k = 3 reductions
│   ├── Order2Input.lean             # Repaired Larsen-Larsen order-two input
│   ├── ClusteredInput.lean          # Finite-shift clustered order-three input
│   ├── ProbabilityTools.lean        # Probability and concentration utilities
│   ├── ClaudeProbCore.lean          # Core probabilistic estimates
│   ├── LLProp5AntiClustering.lean   # Anti-clustering argument
│   └── LarsenLarsenL7BC.lean        # Lemma 7 and Borel-Cantelli support
├── paper/
│   ├── erdos_870_paper.pdf          # Paper
│   ├── erdos_870_paper.tex          # LaTeX source
│   └── README.md
├── notes/
│   ├── FORMALIZATION_GUIDE.md
│   ├── PAPER_TO_LEAN.md
│   ├── AXIOM_AUDIT.md
│   └── SOURCE_PROVENANCE.md
├── scripts/
│   ├── check_no_placeholders.py
│   ├── check_local_imports.py
│   ├── check_axioms.py
│   └── print_axioms.sh
├── problem_statement.md
├── Makefile
├── lakefile.toml
├── lake-manifest.json
├── lean-toolchain                   # Lean 4.30.0-rc2
├── CITATION.cff
├── NOTICE
└── LICENSE                          # Apache-2.0 for code and repository text

Build and verify

Install elan, then run:

lake exe cache get
make check

The individual commands are:

make imports   # all project-local imports resolve
make audit     # no active sorry/admit or project assumption declarations
make build     # compile the project
make axioms    # print and check final kernel dependencies

Lean and Mathlib are pinned to v4.30.0-rc2, including transitive revisions in lake-manifest.json.

Build the paper

make paper

A pre-built PDF is committed at paper/erdos_870_paper.pdf, so reading the paper does not require a TeX installation.

Trust boundary

The packaged active source passes the included comment-aware static audit with no admitted proof and no project-specific assumption declaration. The final files run #print axioms. CI performs a clean build and checks that the reported dependencies are limited to:

[propext, Classical.choice, Quot.sound]

These are standard Lean principles used through Mathlib. See notes/AXIOM_AUDIT.md.

Relationship to Problem #868

The order-two input builds on Daniel Larsen and Michael Larsen's negative answer to Erdős Problem #868. A separate standalone repository will package that theorem in its exact two-summand form and will include their paper with explicit attribution.

Citation

@misc{turturean2026erdos870,
  author       = {David Turturean},
  title        = {Additive bases with many representations and no minimal subbasis: A negative answer to Erdős Problem #870},
  year         = {2026},
  howpublished = {GitHub repository},
  url          = {https://github.com/davidturturean/erdos-870}
}

See CITATION.cff for machine-readable metadata.

License and disclosure

The Lean code and repository documentation are licensed under Apache-2.0. The paper remains copyright David Turturean. The natural-language proof used GPT-5.4-Pro then GPT-5.5-Pro; the Lean formalization used GPT-5.5-Pro, Codex (GPT-5.5-xhigh), and Claude Code (Opus 4.8, maximum thinking). Compute was provided by Fulcrum. David Turturean is responsible for the final mathematical claims and exposition. See LICENSE and NOTICE.