10.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 6 contain sorry, 0 declared as axioms

Erdős Problem 10

References:

erdosproblems.com/10
[Cr71] Crocker, R., On the sum of a prime and of two powers of two. Pacific J. Math. 36 (1971), 103-107.
[Ga75] Gallagher, P. X., Primes and powers of 2. Acta Arith. 29 (1976), 353-370.
[GrSo98] Granville, A. and Soundararajan, K., A binary additive problem of Erdős and the order of $2$ mod $p^2$. Ramanujan J. 2 (1998), 283-298.

Imports (1)

FormalConjecturesUtil

abbrev Erdos10.sumPrimeAndTwoPows The set of natural numbers that can be written as a sum of a prime and at most $k$ powers of $2$ line 42 source
Source documentation
The set of natural numbers that can be written as a sum of a prime and at most $k$ powers of $2$.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: Set.ofPred, Exists, Multiset, Nat.Prime, LE.le, Multiset.card, Eq, HAdd.hAdd, Multiset.sum, Multiset.map, HPow.hPow, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
abbrev sumPrimeAndTwoPows (k : ℕ) : Set ℕ :=
…
```
theorem Erdos10.two_mem_sumPrimeAndTwoPows_zero A prime is the sum of a prime and no powers of $2$ line 48 source
Source documentation
A prime is the sum of a prime and no powers of $2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Nat, Set, Erdos10.sumPrimeAndTwoPows, OfNat.ofNat
Proof uses: Exists.intro, Exists, Multiset, Nat.Prime, LE.le, Multiset.card, Eq, HAdd.hAdd, Multiset.sum, Multiset.map, HPow.hPow, Nat.prime_two, of_eq_true, Eq.trans, True, congrFun', congrArg, add_zero, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem two_mem_sumPrimeAndTwoPows_zero : 2 ∈ sumPrimeAndTwoPows 0 :=
…
```
Mentions: Erdos10.sumPrimeAndTwoPows
theorem Erdos10.one_not_mem_sumPrimeAndTwoPows $1$ is smaller than every prime, so it lies in no sumPrimeAndTwoPows k line 53 source
Source documentation
$1$ is smaller than every prime, so it lies in no sumPrimeAndTwoPows k.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Not, Membership.mem, Set, Erdos10.sumPrimeAndTwoPows, OfNat.ofNat
Proof uses: Exists, Multiset, Nat.Prime, LE.le, Multiset.card, Eq, HAdd.hAdd, Multiset.sum, Multiset.map, HPow.hPow, False, Nat.Prime.two_le
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem one_not_mem_sumPrimeAndTwoPows (k : ℕ) : 1 ∉ sumPrimeAndTwoPows k := by
…
```
Mentions: Erdos10.sumPrimeAndTwoPows
theorem Erdos10.erdos_10 Is there some $k$ such that every large integer is the sum of a prime and at most $k$ powers of $2$? sorry line 63 source
Source documentation
Is there some $k$ such that every large integer is the sum of a prime and at most $k$ powers of $2$?

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Filter.Eventually, Membership.mem, Set, Erdos10.sumPrimeAndTwoPows, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_10 : answer(sorry) ↔ ∃ k, ∀ᶠ n : ℕ in atTop, n ∈ sumPrimeAndTwoPows k := by
…
```
Mentions: Erdos10.sumPrimeAndTwoPows
theorem Erdos10.erdos_10.variants.gallagher Documented declaration: gallagher sorry line 74 source
Source documentation
Gallagher [Ga75] has shown that for any $ϵ > 0$ there exists $k(ϵ)$ such that the set of integers which are the sum of a prime and at most $k(ϵ)$ many powers of $2$ has lower density at least $1 - ϵ$.
Ref: Gallagher, P. X., Primes and powers of 2.

depends on sorry what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Exists, Nat, LE.le, HSub.hSub, Set.lowerDensity, Erdos10.sumPrimeAndTwoPows, Set.univ
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_10.variants.gallagher (ε : ℝ)
    (hε : 0 < ε) : ∃ k, 1 - ε ≤ (sumPrimeAndTwoPows k).lowerDensity := by
…
```
Mentions: Erdos10.sumPrimeAndTwoPows
theorem Erdos10.erdos_10.variants.granville_soundararajan_odd Granville and Soundararajan [GrSo98] have conjectured that at most sorry line 86 source
Source documentation
Granville and Soundararajan [GrSo98] have conjectured that at most $3$ powers of $2$ suffice for all odd integers, and hence at most $4$ powers of $2$ suffice for all even integers.
Ref: Granville, A. and Soundararajan, K., A Binary Additive Problem of Erdős and the Order of $2$ mod $p^2$

depends on sorry what this means
Statement uses: And, LE.le, Set, Nat, Set.ofPred, Odd, LT.lt, OfNat.ofNat, Erdos10.sumPrimeAndTwoPows, Even, Ne
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_10.variants.granville_soundararajan_odd :
    {n : ℕ | Odd n ∧ 1 < n} ⊆ sumPrimeAndTwoPows 3 ∧
      {n : ℕ | Even n ∧ n ≠ 0} ⊆ sumPrimeAndTwoPows 4 := by
…
```
Mentions: Erdos10.sumPrimeAndTwoPows
theorem Erdos10.erdos_10.variants.grechuk_example Bogdan Grechuk has observed that 1117175146 is not the sum of a prime and at most $3$ powers of $2$ sorry line 96 source
Source documentation
Bogdan Grechuk has observed that 1117175146 is not the sum of a prime and at most $3$ powers of $2$.

depends on sorry what this means
Statement uses: Not, Membership.mem, Nat, Set, Erdos10.sumPrimeAndTwoPows, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_10.variants.grechuk_example :
    1117175146 ∉ sumPrimeAndTwoPows 3 := by
…
```
Mentions: Erdos10.sumPrimeAndTwoPows
theorem Erdos10.erdos_10.variants.two_pows There are infinitely many even integers not the sum of a prime and $2$ powers of $2$ sorry line 104 source
Source documentation
There are infinitely many even integers not the sum of a prime and $2$ powers of $2$

depends on sorry what this means
Statement uses: Set.Infinite, Nat, SDiff.sdiff, Set, Set.ofPred, Even, Erdos10.sumPrimeAndTwoPows, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_10.variants.two_pows :
    Set.Infinite <| {n : ℕ | Even n} \ sumPrimeAndTwoPows 2 := by
…
```
Mentions: Erdos10.sumPrimeAndTwoPows
theorem Erdos10.erdos_10.variants.grechuk sorry line 122 source
depends on sorry what this means
Statement uses: Set.Infinite, Nat, SDiff.sdiff, Set, Set.ofPred, Even, Erdos10.sumPrimeAndTwoPows, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.