cff-version: 1.2.0
message: "If you reference this solution, paper, or formalization, please cite it as below."
title: "Additive bases with many representations and no minimal subbasis: A negative answer to Erdős Problem #870"
version: 1.0.0
authors:
  - family-names: "Turturean"
    given-names: "David Corneliu"
    affiliation: "Fulcrum"
    email: "davidct@mit.edu"
date-released: 2026-06-18
license: Apache-2.0
repository-code: "https://github.com/davidturturean/erdos-870"
abstract: >-
  For every k >= 3 and C > 0, this repository constructs and formalizes an
  additive basis of order at most k with at least C log n representations for
  all sufficiently large n and with no minimal order-k subbasis. It contains
  the paper and a Lean 4 formalization against Mathlib v4.30.0.
keywords:
  - "Erdős problem"
  - "additive basis"
  - "Lean 4"
  - "formal verification"
  - "probabilistic method"