67836.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

17 declarations, 1 contain sorry, 0 declared as axioms

Euclid–Fortunate prime coverage

OEIS A067836 starts with $2$. Each later term is the gap from the product of all previous terms to the least prime strictly greater than that product plus one.

References:

OEIS A067836

Imports (1)

FormalConjecturesUtil

def OeisA67836.primeCandidates The finite set in which the least prime strictly above n is sought line 36 source
Source documentation
The finite set in which the least prime strictly above n is sought.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.filter, Nat.Prime, Finset.Icc, HAdd.hAdd, OfNat.ofNat, HMul.hMul
8 instances, coercions and auxiliary constants left out.
```
def primeCandidates (n : ℕ) : Finset ℕ :=
…
```
lemma OeisA67836.primeCandidates_nonempty Bertrand's postulate makes the finite prime-candidate set nonempty line 41 source
Source documentation
Bertrand's postulate makes the finite prime-candidate set nonempty.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset.Nonempty, OeisA67836.primeCandidates
Proof uses: And, Nat.Prime, LT.lt, HAdd.hAdd, OfNat.ofNat, LE.le, HMul.hMul, Exists, Nat.bertrand, Eq, Exists.intro, Membership.mem, Finset, Eq.mpr, id, Eq.trans, Finset.filter, Finset.Icc, congrFun', congrArg and 3 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma primeCandidates_nonempty (n : ℕ) : (primeCandidates n).Nonempty := by
…
```
Mentions: OeisA67836.primeCandidates
def OeisA67836.leastPrimeAbove The least prime strictly greater than n, found in the Bertrand interval line 48 source
Source documentation
The least prime strictly greater than n, found in the Bertrand interval.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.min', OeisA67836.primeCandidates, OeisA67836.primeCandidates_nonempty
1 instances, coercions and auxiliary constants left out.
```
def leastPrimeAbove (n : ℕ) : ℕ :=
…
```
lemma OeisA67836.leastPrimeAbove_spec The chosen number is strictly above the bound and is prime line 53 source
Source documentation
The chosen number is strictly above the bound and is prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LT.lt, OeisA67836.leastPrimeAbove, Nat.Prime
Proof uses: Membership.mem, Finset, OeisA67836.primeCandidates, Finset.min', OeisA67836.primeCandidates_nonempty, Finset.min'_mem, Eq.mpr, LE.le, HAdd.hAdd, OfNat.ofNat, Finset.filter, Finset.Icc, HMul.hMul, Finset.Nonempty, id, Eq, Eq.refl, And.left, Eq.mp, Eq.trans and 4 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma leastPrimeAbove_spec (n : ℕ) :
    n < leastPrimeAbove n ∧ (leastPrimeAbove n).Prime := by
…
```
Mentions: OeisA67836.leastPrimeAbove
lemma OeisA67836.leastPrimeAbove_le The least prime above n is no larger than any other prime above n line 65 source
Source documentation
The least prime above n is no larger than any other prime above n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Nat.Prime, LE.le, OeisA67836.leastPrimeAbove
Proof uses: dite, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Membership.mem, Finset, OeisA67836.primeCandidates, Eq.mpr, And, id, Eq, Eq.trans, Finset.filter, Finset.Icc, congrFun', congrArg, And.intro, Decidable.byContradiction, Not, Finset.min'_le and 8 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma leastPrimeAbove_le (n p : ℕ) (hnp : n < p) (hp : p.Prime) :
    leastPrimeAbove n ≤ p := by
…
```
Mentions: OeisA67836.leastPrimeAbove
lemma OeisA67836.not_prime_of_lt_leastPrimeAbove No number strictly between n and leastPrimeAbove n is prime line 80 source
Source documentation
No number strictly between n and leastPrimeAbove n is prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OeisA67836.leastPrimeAbove, Not, Nat.Prime
Proof uses: LE.le, OeisA67836.leastPrimeAbove_le
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma not_prime_of_lt_leastPrimeAbove (n p : ℕ) (hnp : n < p)
    (hp : p < leastPrimeAbove n) : ¬ p.Prime := by
…
```
Mentions: OeisA67836.leastPrimeAbove
lemma OeisA67836.leastPrimeAbove_eq A convenient criterion for computing the least prime above a concrete bound line 88 source
Source documentation
A convenient criterion for computing the least prime above a concrete bound.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Nat.Prime, Not, Eq, OeisA67836.leastPrimeAbove
Proof uses: Nat.le_antisymm, OeisA67836.leastPrimeAbove_le, Decidable.byContradiction, LE.le, And.left, OeisA67836.leastPrimeAbove_spec, And.right
6 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma leastPrimeAbove_eq (n p : ℕ) (hnp : n < p) (hp : p.Prime)
    (hmin : ∀ q, n < q → q < p → ¬ q.Prime) : leastPrimeAbove n = p := by
…
```
Mentions: OeisA67836.leastPrimeAbove
structure OeisA67836.State The recursive state records the latest term and the product of all official terms so far line 96 source
Source documentation
The recursive state records the latest term and the product of all official terms so far.

no axioms what this means
```
structure State where
…
```
def OeisA67836.state The state after n official terms, with the empty state initialized by term and product one line 101 source
Source documentation
The state after n official terms, with the empty state initialized by term and product one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OeisA67836.State
2 instances, coercions and auxiliary constants left out.
```
def state : ℕ → State
  | 0 => ⟨1, 1⟩
  | n + 1 =>
      let previous := state n
…
```
Mentions: OeisA67836.State
def OeisA67836.a OEIS A067836, with the convenience value a 0 = 1 preceding its official first term line 109 source
Source documentation
OEIS A067836, with the convenience value a 0 = 1 preceding its official first term.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: OeisA67836.State.term, OeisA67836.state
```
def a (n : ℕ) : ℕ :=
…
```
theorem OeisA67836.a_0 line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, OeisA67836.a, OfNat.ofNat
Proof uses: Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OeisA67836.a_1 line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, OeisA67836.a, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OeisA67836.a_2 line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, OeisA67836.a, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OeisA67836.a_3 line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, OeisA67836.a, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OeisA67836.a_4 line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, OeisA67836.a, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OeisA67836.a_5 line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, OeisA67836.a, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OeisA67836.conjecture OEIS A067836 asks: "Do all primes occur in the sequence?" sorry line 138 source
Source documentation
OEIS A067836 asks: "Do all primes occur in the sequence?"

L4DEL explanation
OEIS A067836 asks: "Do all primes occur in the sequence?"
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, True, Nat, Nat.Prime, Exists, And, GE.ge, OfNat.ofNat, Eq, OeisA67836.a
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 conjecture :
    answer(sorry) ↔ ∀ p, p.Prime → ∃ n ≥ 1, a n = p := by
…
```
Mentions: OeisA67836.a