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

7 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 313

References:

erdosproblems.com/313
A54377 (Primary pseudoperfect numbers)

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

def Erdos313.erdos313Solutions This set contains all solutions (m, P) to the Erdős problem 313 line 37 source
Source documentation
This set contains all solutions (m, P) to the Erdős problem 313. A solution is a pair where m is an integer ≥ 2 and P is a non-empty, finite set of distinct prime numbers, such that the sum of the reciprocals of the primes in P equals 1 - 1/m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Prod, Nat, Finset
Proof uses: Set.ofPred, Erdos313.erdos313Solutions.match_1, And, LE.le, OfNat.ofNat, Finset.Nonempty, Membership.mem, Nat.Prime, Eq, Rat, Finset.sum, HDiv.hDiv, HSub.hSub
12 instances, coercions and auxiliary constants left out.
```
def erdos313Solutions : Set (ℕ × Finset ℕ) :=
…
```
theorem Erdos313.erdos_313 Are there infinitely many pairs (m, P) where m ≥ 2 is an integer and P is a set of distinct primes such that the following equation holds sorry line 46 source
Source documentation
Are there infinitely many pairs (m, P) where m ≥ 2 is an integer and P is a set of distinct primes such that the following equation holds: $\sum_{p \in P} \frac{1}{p} = 1 - \frac{1}{m}$?

depends on sorry what this means
Statement uses: Iff, True, Set.Infinite, Prod, Nat, Finset, Erdos313.erdos313Solutions
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_313 : answer(sorry) ↔ erdos313Solutions.Infinite := by
…
```
theorem Erdos313.erdos_313.variants.solution_6_2_3 line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Prod, Nat, Finset, Set, Erdos313.erdos313Solutions, Prod.mk, OfNat.ofNat, Insert.insert, Singleton.singleton
Proof uses: of_eq_true, Eq.trans, Set.ofPred, And, LE.le, Prod.fst, Finset.Nonempty, Prod.snd, Nat.Prime, Eq, Rat, Finset.sum, Inv.inv, HSub.hSub, True, congrFun', congrArg, Erdos313.erdos313Solutions.match_1, HDiv.hDiv, funext and 45 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos313.erdos_313.variants.solution_42_2_3_7 line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Prod, Nat, Finset, Set, Erdos313.erdos313Solutions, Prod.mk, OfNat.ofNat, Insert.insert, Singleton.singleton
Proof uses: of_eq_true, Eq.trans, Set.ofPred, And, LE.le, Prod.fst, Finset.Nonempty, Prod.snd, Nat.Prime, Eq, Rat, Finset.sum, Inv.inv, HSub.hSub, True, congrFun', congrArg, Erdos313.erdos313Solutions.match_1, HDiv.hDiv, funext and 47 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Erdos313.IsPrimaryPseudoperfect An integer n is a primary pseudoperfect number if it is the denominator m in a solution (m, P) to the Erdős 313 problem line 61 source
Source documentation
An integer n is a primary pseudoperfect number if it is the denominator m in a solution (m, P) to the Erdős 313 problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Finset, Membership.mem, Prod, Set, Erdos313.erdos313Solutions, Prod.mk
1 instances, coercions and auxiliary constants left out.
```
def IsPrimaryPseudoperfect (n : ℕ) : Prop := ∃ P, (n, P) ∈ erdos313Solutions
…
```
Mentions: Erdos313.erdos313Solutions
theorem Erdos313.erdos_313.variants.primary_pseudoperfect_are_infinite It is conjectured that the set of primary pseudoperfect numbers is infinite sorry line 67 source
Source documentation
It is conjectured that the set of primary pseudoperfect numbers is infinite.

depends on sorry what this means
Statement uses: Set.Infinite, Nat, Set.ofPred, Erdos313.IsPrimaryPseudoperfect
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_313.variants.primary_pseudoperfect_are_infinite :
    Set.Infinite {n | IsPrimaryPseudoperfect n} := by
…
```
Mentions: Erdos313.IsPrimaryPseudoperfect
theorem Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect There are at least 8 primary pseudoperfect numbers line 77 source
Source documentation
There are at least 8 primary pseudoperfect numbers. The first eight terms of A54377 are exhibited together with their explicit prime decompositions.

L4DEL explanation
There are at least 8 primary pseudoperfect numbers. The first eight terms of A54377 are exhibited together with their explicit prime decompositions.
Sources and attribution: Pinned Lean source (1646ca16afd6)

extra axioms: _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_10, _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_2, _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_3, _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_4, _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_5, _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_6, _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_7, _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_8, _private.0.Erdos313.erdos_313.variants.exists_at_least_eight_primary_pseudoperfect._native.native_decide.ax_9 what this means
Statement uses: LE.le, ENat, OfNat.ofNat, Nat, Set.encard, Set.ofPred, Erdos313.IsPrimaryPseudoperfect
Proof uses: Finset, Insert.insert, Singleton.singleton, Set, Membership.mem, Eq, Or, Eq.mp, Eq.trans, congrFun', congrArg, Finset.coe_insert, Finset.coe_singleton, Exists.intro, Prod, Erdos313.erdos313Solutions, Prod.mk, of_eq_true, And, Prod.fst and 82 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_313.variants.exists_at_least_eight_primary_pseudoperfect :
    8 ≤ (Set.encard {n | IsPrimaryPseudoperfect n}) := by
…
```
Mentions: Erdos313.IsPrimaryPseudoperfect