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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 971

Reference: erdosproblems.com/971

Imports (1)

FormalConjecturesUtil

def Erdos971.leastCongruentPrime leastCongruentPrime a d is the least prime congruent to a modulo d line 33 source
Source documentation
leastCongruentPrime a d is the least prime congruent to a modulo d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Set.ofPred, And, Nat.Prime, Nat.ModEq
1 instances, coercions and auxiliary constants left out.
```
noncomputable def leastCongruentPrime (a d : ℕ) : ℕ :=
…
```
theorem Erdos971.erdos_971 Let p(a, d) be the least prime congruent to a (mod d) sorry line 42 source
Source documentation
Let p(a, d) be the least prime congruent to a (mod d). Does there exist a constant c > 0 such that for all large d, p(a, d) > (1 + c) * φ(d) * log d for ≫ φ(d) many values of a?

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, HMul.hMul, Nat.totient, Finset.card, Finset.filter, Nat.Coprime, Erdos971.leastCongruentPrime, HAdd.hAdd, Real.log, Finset.Iio, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_971 : answer(sorry) ↔
    ∃ c > (0 : ℝ), ∃ C > (0 : ℝ), ∀ᶠ d in atTop,
      C * (d.totient : ℝ) ≤
        #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) > (1 + c) * d.totient * log d} := by
…
```
Mentions: c, Erdos971.leastCongruentPrime
theorem Erdos971.erdos_971.variants.infinite_sequence Erdős [Er49c] proved that the statement in erdos_971 holds for infinitely many values of d sorry line 55 source
Source documentation
Erdős [Er49c] proved that the statement in erdos_971 holds for infinitely many values of d.
[Er49c] Erdős, P., On some applications of Brun's method. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57--63.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Set.Infinite, Nat, Set.ofPred, LE.le, HMul.hMul, Nat.totient, Finset.card, Finset.filter, Nat.Coprime, Erdos971.leastCongruentPrime, HAdd.hAdd, Real.log, Finset.Iio
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_971.variants.infinite_sequence :
    ∃ c > (0 : ℝ), ∃ C > (0 : ℝ),
      {d : ℕ | C * (d.totient : ℝ) ≤
        #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) > (1 + c) * d.totient * log d}}.Infinite :=
…
```
Mentions: c, Erdos971.leastCongruentPrime
theorem Erdos971.erdos_971.variants.many_small Erdős [Er49c] proved that for any ε > 0 we have p(a, d) < ε * φ(d) * log d for ≫_ε φ(d) many values of a (for all large d) sorry line 70 source
Source documentation
Erdős [Er49c] proved that for any ε > 0 we have p(a, d) < ε * φ(d) * log d for ≫_ε φ(d) many values of a (for all large d).
[Er49c] Erdős, P., On some applications of Brun's method. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57--63.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, And, Filter.Eventually, Nat, LE.le, HMul.hMul, Nat.totient, Finset.card, Finset.filter, Nat.Coprime, LT.lt, Erdos971.leastCongruentPrime, Real.log, Finset.Iio, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_971.variants.many_small :
    ∀ ε > (0 : ℝ), ∃ C > (0 : ℝ), ∀ᶠ d in atTop,
      C * (d.totient : ℝ) ≤
        #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) < ε * d.totient * log d} := by
…
```
Mentions: Erdos971.leastCongruentPrime