erdos_741.parts.i.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 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were 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 source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

121 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

FormalConjectures.Util.ProblemImports

def Erdos741.S_x The lower observation scale in the Erdős 741 counterexample line 79 source
L4DEL explanation
The key point is that B1 + B2 = N0 , while the long intervals Ik force large local oscillations
— Ulam AI, A Note on Erdős Problem #741 (2026)
S_x(k)=4^(3^k) is the rapidly growing left endpoint of the kth scale. Base four makes the digit split carry-free, while the double-exponential spacing prevents earlier added intervals from controlling the next density measurement.
1. Raise 4 to 3^k; the resulting scales race apart.
2. At 2*S_x(k), the proof measures how sparse the two monochromatic self-sumsets still are.
3. This Lean artifact uses the fixed-factor companion scale S_y(k)=10*S_x(k); Ulam AI's written proof uses longer k*N_k intervals and explicitly distinguishes the constructions.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def S_x (k : ℕ) : ℕ := 4 ^ (3 ^ k)
```
def Erdos741.S_y The upper endpoint: ten times the lower scale line 80 source
L4DEL explanation
Our proof uses the same underlying mechanism, but chooses the intervals Ik with length kNk rather than a fixed multiple of Nk .
— Ulam AI, A Note on Erdős Problem #741 (2026)
S_y(k)=10*S_x(k) gives each added interval a fixed nine-scale-unit width. Those fat intervals later force many same-colour sums before the next enormous base-four scale arrives.
1. Start at S_x(k) and end at ten times that value.
2. Compare partial densities at 2*S_x(k) and 2*S_y(k).
3. Do not identify this fixed-multiple construction with Ulam AI's fully written variant, whose interval length grows like k*N_k; the note says they share a mechanism, not identical intervals.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HMul.hMul, OfNat.ofNat, HPow.hPow
6 instances, coercions and auxiliary constants left out.
```
def S_y (k : ℕ) : ℕ := 10 * 4 ^ (3 ^ k)
```
def Erdos741.S_C The sparse union of fat intervals that drives density oscillation line 82 source
L4DEL explanation
The key point is that B1 + B2 = N0 , while the long intervals Ik force large local oscillations
— Ulam AI, A Note on Erdős Problem #741 (2026)
S_C is the union of every half-open interval [S_x(k),S_y(k)). Each interval is locally large, but the starting scales grow so quickly that earlier intervals become negligible at the next lower checkpoint.
1. Insert the full interval from S_x(k) through S_y(k)-1 for every k.
2. The intervals later provide a large block in whichever colour receives their elements.
3. Their separation lets the proof alternate between sparse lower-scale behavior and dense upper-scale behavior.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: propext what this means
Statement uses: Set, Nat
Proof uses: Set.iUnion, Set.Ico, Erdos741.S_x, Erdos741.S_y
1 instances, coercions and auxiliary constants left out.
```
def S_C : Set ℕ := ⋃ k, Ico (S_x k) (S_y k)
```
Mentions: Erdos741.S_x, Erdos741.S_y
def Erdos741.split1 Put each binary digit into the 0-or-1 part of a base-four number line 84 source
L4DEL explanation
Every digit d ∈ {0, 1, 2, 3} has a unique decomposition
— Ulam AI, A Note on Erdős Problem #741 (2026)
split1(n) recursively keeps the parity bit of each base-four digit. Its base-four digits are therefore only 0 or 1, which prevents carries when two B1 elements are added.
1. Take n % 2 as the current low digit.
2. Recurse on n/4, shifting the result left by one base-four place.
3. Paired with split2, the two digit streams add back to the original natural number.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, Eq, OfNat.ofNat, Not, HAdd.hAdd, HMod.hMod, HMul.hMul, HDiv.hDiv
12 instances, coercions and auxiliary constants left out.
```
noncomputable def split1 (n : ℕ) : ℕ :=
…
```
def Erdos741.split2 Put the complementary 0-or-2 contribution into the second base-four stream line 88 source
L4DEL explanation
Every digit d ∈ {0, 1, 2, 3} has a unique decomposition
— Ulam AI, A Note on Erdős Problem #741 (2026)
split2(n) keeps n % 4 - n % 2 at each digit, so its base-four digits are 0 or 2. Digit by digit, split1(n)+split2(n)=n without a carry.
1. Remove the parity contribution from the current base-four digit.
2. Recurse on n/4 and shift by a factor of four.
3. The complementary digits are the coverage half of the construction; each half's self-sums remain sparse.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, Eq, OfNat.ofNat, Not, HAdd.hAdd, HSub.hSub, HMod.hMod, HMul.hMul, HDiv.hDiv
14 instances, coercions and auxiliary constants left out.
```
noncomputable def split2 (n : ℕ) : ℕ :=
…
```
def Erdos741.B1 The carry-free base-four set with digits 0 and 1 line 92 source
L4DEL explanation
The key point is that B1 + B2 = N0 , while the long intervals Ik force large local oscillations
— Ulam AI, A Note on Erdős Problem #741 (2026)
B1 is the range of split1. Its elements use only 0-or-1 base-four digits, making B1+B1 digitwise sparse even though B1+B2 will cover every natural number.
1. Collect every output of split1.
2. Two such outputs can only produce base-four sum digits 0, 1, or 2.
3. This supplies one sparse monochromatic channel in the partition argument.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.range, Erdos741.split1
```
def B1 : Set ℕ := Set.range split1
```
Mentions: Erdos741.split1
def Erdos741.B2 The complementary carry-free base-four set with digits 0 and 2 line 93 source
L4DEL explanation
The key point is that B1 + B2 = N0 , while the long intervals Ik force large local oscillations
— Ulam AI, A Note on Erdős Problem #741 (2026)
B2 is the range of split2. It is the digitwise complement to B1: together the two sets represent every natural, while B2+B2 has the same sparse-count phenomenon as B1+B1.
1. Collect every output of split2.
2. Its digits are 0 or 2, equivalently twice the 0-or-1 digit pattern.
3. Pair each split2(n) with split1(n) to recover n.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.range, Erdos741.split2
```
def B2 : Set ℕ := Set.range split2
```
Mentions: Erdos741.split2
def Erdos741.B line 94 source
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Union.union, Erdos741.B1, Erdos741.B2
1 instances, coercions and auxiliary constants left out.
def Erdos741.SandorA The strict-natural-density counterexample set line 96 source
L4DEL explanation
Our proof uses the same underlying mechanism, but chooses the intervals Ik with length kNk rather than a fixed multiple of Nk .
— Ulam AI, A Note on Erdős Problem #741 (2026)
SandorA joins the carry-free covering set B1∪B2 to the sparse union of fat intervals S_C. Coverage makes SandorA+SandorA all naturals; the intervals make every two-colouring oscillate too much for both monochromatic self-sumsets to have positive natural-density limits.
1. Begin with B1∪B2, whose cross-sums cover all naturals.
2. Add the fixed-factor intervals [S_x(k),S_y(k)), with S_y(k)=10*S_x(k), to force large local blocks of same-colour sums.
3. Use widely separated checkpoints to turn these two features into a convergence contradiction.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Union.union, Erdos741.B, Erdos741.S_C
1 instances, coercions and auxiliary constants left out.
```
def SandorA : Set ℕ := B ∪ S_C
```
Mentions: Erdos741.B, Erdos741.S_C
lemma Erdos741.split1_bound line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Erdos741.split1, HMul.hMul
Proof uses: Nat.strongRecOn, LT.lt, dite, Eq, OfNat.ofNat, Eq.mpr, id, congrArg, Not, HAdd.hAdd, HMod.hMod, HDiv.hDiv, Erdos741.split1.eq_def, of_eq_true, Eq.trans, True, congr, dite_cond_eq_true, eq_self, MulZeroClass.mul_zero and 39 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_mod line 141 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, Erdos741.split1, OfNat.ofNat
Proof uses: HAdd.hAdd, HMul.hMul, HDiv.hDiv, dite, Eq.mpr, id, congrArg, Not, congr, Erdos741.split1.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, Nat.zero_div, MulZeroClass.mul_zero, add_zero, Erdos741.split1.eq_1, dite_cond_eq_false and 2 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_sum_mod line 151 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMod.hMod, HAdd.hAdd, Erdos741.split1, OfNat.ofNat
Proof uses: Eq, Erdos741.split1_mod, Decidable.byContradiction, Not, HMul.hMul, HDiv.hDiv, LT.lt
27 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_div line 162 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HDiv.hDiv, Erdos741.split1, OfNat.ofNat
Proof uses: HAdd.hAdd, HMod.hMod, HMul.hMul, dite, Eq.mpr, id, congrArg, Not, congr, Erdos741.split1.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, Nat.zero_div, MulZeroClass.mul_zero, add_zero, Erdos741.split1.eq_1, dite_cond_eq_false and 2 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_sum_div line 172 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HDiv.hDiv, HAdd.hAdd, Erdos741.split1, OfNat.ofNat
Proof uses: HMod.hMod, HMul.hMul, dite, Eq.mpr, id, congrArg, Not, congr, Erdos741.split1.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, Nat.zero_div, MulZeroClass.mul_zero, add_zero, Erdos741.split1.eq_1, dite_cond_eq_false, eq_false and 1 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_sum_digit line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMod.hMod, HDiv.hDiv, HAdd.hAdd, Erdos741.split1, HPow.hPow, OfNat.ofNat
Proof uses: Nat.recAux, Eq.mpr, id, Eq, congrArg, Nat.div_one, Erdos741.B1_sum_mod, HMul.hMul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.pow_add and 16 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_sum_no_digit3 line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, HAdd.hAdd, Erdos741.B1, Ne, HMod.hMod, HDiv.hDiv, HPow.hPow, OfNat.ofNat
Proof uses: And, Exists, Eq, Erdos741.split1, LE.le, Erdos741.B1_sum_digit, of_decide_eq_true, False, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mp, congrArg
31 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Erdos741.base3_to_base4 line 211 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, Eq, OfNat.ofNat, Not, HAdd.hAdd, HMod.hMod, HMul.hMul, HDiv.hDiv
12 instances, coercions and auxiliary constants left out.
lemma Erdos741.base3_to_base4_bound line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Erdos741.base3_to_base4
Proof uses: Nat.recAux, Eq, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, dite, HAdd.hAdd, HMod.hMod, HMul.hMul, HDiv.hDiv, Erdos741.base3_to_base4.eq_def, of_eq_true, Eq.trans, True, congr, dite_cond_eq_true, eq_self, pow_zero and 35 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.base3_to_base4_lt_4_pow line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, Erdos741.base3_to_base4
Proof uses: Erdos741.base3_to_base4_bound
10 instances, coercions and auxiliary constants left out.
lemma Erdos741.missing_3_exists_base3 line 243 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, HMod.hMod, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Exists, Eq, Erdos741.base3_to_base4
Proof uses: Nat.strongRecOn, LT.lt, dite, Exists.intro, Eq.mpr, id, congrArg, Not, HAdd.hAdd, HMul.hMul, Erdos741.base3_to_base4.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, Decidable.byContradiction, Eq.mp, Nat.div_one, Mathlib.Tactic.Ring.of_eq and 34 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.base3_to_base4_lt_4_pow_iff line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, LT.lt, Erdos741.base3_to_base4, HPow.hPow, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, propext, Nat.pow_lt_pow_iff_left, LT.lt.ne', Nat.two_pow_pos, dite, Not, HAdd.hAdd, HMod.hMod, HMul.hMul, HDiv.hDiv, Erdos741.base3_to_base4.eq_1, Trans.simple, WellFounded.Nat.fix, InvImage, Nat.ofDigits and 89 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_sum_subset_image line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, HasSubset.Subset, Set, Inter.inter, HAdd.hAdd, Erdos741.B1, Set.Iio, HPow.hPow, OfNat.ofNat, Set.image, Erdos741.base3_to_base4
Proof uses: Membership.mem, And.left, LT.lt, And.right, Ne, HMod.hMod, HDiv.hDiv, Erdos741.B1_sum_no_digit3, Eq, Exists, Erdos741.missing_3_exists_base3, Exists.intro, And, And.intro, Decidable.byContradiction, Not, Iff.mp, Erdos741.base3_to_base4_lt_4_pow_iff, Eq.symm
28 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_sum_ncard Below 4^d, the first self-sumset has at most 3^d values line 312 source
L4DEL explanation
Every digit d ∈ {0, 1, 2, 3} has a unique decomposition
— Ulam AI, A Note on Erdős Problem #741 (2026)
A sum of two 0-or-1 base-four digit strings never has digit 3. There are only three choices at each of the first d positions, hence at most 3^d possible sums below 4^d.
1. Prove each base-four digit of a B1+B1 value lies in {0,1,2}.
2. Encode those d digits as a base-three number.
3. Injectivity gives the cardinality bound 3^d, negligible beside 4^d.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Set.ncard, Inter.inter, Set, HAdd.hAdd, Erdos741.B1, Set.Iio, HPow.hPow, OfNat.ofNat
Proof uses: HasSubset.Subset, Set.image, Erdos741.base3_to_base4, Erdos741.B1_sum_subset_image, Set.Finite, Set.finite_Iio, Set.ncard_image_le, Eq, of_eq_true, Eq.trans, True, congrArg, Nat.ncard_Iio, eq_self, eq_true, True.intro, Set.ncard_le_ncard, Set.Finite.image, Decidable.byContradiction, Not
26 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma B1_sum_ncard (d : ℕ) : ((B1 + B1) ∩ Iio (4^d)).ncard ≤ 3^d := by
…
```
Mentions: Erdos741.B1
lemma Erdos741.split2_even line 321 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, Erdos741.split2, OfNat.ofNat
Proof uses: Nat.strongRecOn, LT.lt, dite, Eq.mpr, id, congrArg, Not, HAdd.hAdd, HSub.hSub, HMul.hMul, HDiv.hDiv, Erdos741.split2.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, Erdos741.split2.eq_1, dite_cond_eq_false, eq_false and 1 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B2_sum_even line 335 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, HAdd.hAdd, Erdos741.split2, OfNat.ofNat
Proof uses: Erdos741.split2_even, Decidable.byContradiction, Not
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split2_eq_two_mul_split1 line 340 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos741.split2, HMul.hMul, OfNat.ofNat, Erdos741.split1, HDiv.hDiv
Proof uses: Nat.strongRecOn, LT.lt, dite, Eq.mpr, id, congrArg, Not, HAdd.hAdd, HSub.hSub, HMod.hMod, Erdos741.split2.eq_def, Erdos741.split1.eq_def, of_eq_true, Eq.trans, True, congr, dite_cond_eq_true, eq_self, Nat.zero_div, MulZeroClass.mul_zero and 6 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B2_sum_digit line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HMod.hMod, HDiv.hDiv, HAdd.hAdd, Erdos741.split2, OfNat.ofNat, HPow.hPow
Proof uses: Eq, HMul.hMul, Erdos741.split1, Erdos741.split2_eq_two_mul_split1, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, Erdos741.B1_sum_digit
27 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B2_sum_no_digit3 line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, HAdd.hAdd, Erdos741.B2, Ne, HMod.hMod, HDiv.hDiv, OfNat.ofNat, HPow.hPow
Proof uses: And, Exists, Eq, Erdos741.split2, LE.le, Erdos741.B2_sum_digit, of_decide_eq_true, False, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mp, congrArg
31 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B2_sum_subset_image line 384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, HasSubset.Subset, Set, Inter.inter, HAdd.hAdd, Erdos741.B2, Set.Iio, HPow.hPow, OfNat.ofNat, Set.image, HMul.hMul, Erdos741.base3_to_base4
Proof uses: Membership.mem, And.left, LT.lt, And.right, Eq, HMod.hMod, And, Exists, Erdos741.split2, Erdos741.B2_sum_even, Ne, HDiv.hDiv, Erdos741.B2_sum_no_digit3, Erdos741.missing_3_exists_base3, Exists.intro, And.intro, Trans.trans, LE.le, Eq.symm, Decidable.byContradiction and 7 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B2_sum_ncard The second carry-free self-sumset obeys the same 3^d bound line 406 source
L4DEL explanation
Every digit d ∈ {0, 1, 2, 3} has a unique decomposition
— Ulam AI, A Note on Erdős Problem #741 (2026)
Because the 0-or-2 digit set is twice the 0-or-1 digit set, its self-sums below the matching power-of-four scale also have at most 3^d possibilities.
1. Reduce B2 digits to the corresponding B1 digit pattern.
2. Transfer the no-fourth-digit-choice counting argument.
3. This keeps both pure self-sum channels sparse at the lower checkpoints.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Set.ncard, Inter.inter, Set, HAdd.hAdd, Erdos741.B2, Set.Iio, HPow.hPow, OfNat.ofNat
Proof uses: HasSubset.Subset, Set.image, HMul.hMul, Erdos741.base3_to_base4, Erdos741.B2_sum_subset_image, Set.Finite, Set.finite_Iio, Set.ncard_image_le, Eq, of_eq_true, Eq.trans, True, congrArg, Nat.ncard_Iio, eq_self, eq_true, True.intro, Set.ncard_le_ncard, Set.Finite.image, Decidable.byContradiction and 1 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma B2_sum_ncard (d : ℕ) : ((B2 + B2) ∩ Iio (4^d)).ncard ≤ 3^d := by
…
```
Mentions: Erdos741.B2
lemma Erdos741.split_add line 415 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Erdos741.split1, Erdos741.split2
Proof uses: Nat.strongRecOn, LT.lt, dite, OfNat.ofNat, Eq.mpr, id, congrArg, Not, HMod.hMod, HMul.hMul, HDiv.hDiv, Erdos741.split1.eq_def, HSub.hSub, Erdos741.split2.eq_def, of_eq_true, Eq.trans, True, congr, dite_cond_eq_true, eq_self and 7 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_add_B2_eq_univ The two complementary digit sets add to every natural number line 435 source
L4DEL explanation
Every digit d ∈ {0, 1, 2, 3} has a unique decomposition
— Ulam AI, A Note on Erdős Problem #741 (2026)
For each natural n, the construction splits every base-four digit uniquely between split1(n) and split2(n). Thus n belongs to B1+B2, and the cross-sumset is exactly all naturals.
1. Choose split1(n) from B1 and split2(n) from B2.
2. Apply the digitwise identity split1(n)+split2(n)=n.
3. Since n was arbitrary, conclude B1+B2=Set.univ.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Quot.sound, propext what this means
Statement uses: Eq, Set, Nat, HAdd.hAdd, Erdos741.B1, Erdos741.B2, Set.univ
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, id, Eq.trans, True, congr, congrArg, iff_true, Exists.intro, Erdos741.split1, And.intro, Set.mem_range_self, Erdos741.split2, Erdos741.split_add
9 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma B1_add_B2_eq_univ : B1 + B2 = Set.univ := by
…
```
Mentions: Erdos741.B1, Erdos741.B2
lemma Erdos741.B_add_B_eq_univ line 446 source
standard axioms: Quot.sound, propext what this means
Statement uses: Eq, Set, Nat, HAdd.hAdd, Erdos741.B, Set.univ
Proof uses: HasSubset.Subset, Erdos741.B1, Erdos741.B2, Set.add_subset_add, Set.subset_union_left, Set.subset_union_right, Iff.mp, Set.univ_subset_iff, Eq.mp, congrArg, Erdos741.B1_add_B2_eq_univ
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.SandorA_add_SandorA_eq_univ The counterexample's full self-sumset is all naturals line 451 source
L4DEL explanation
The key point is that B1 + B2 = N0 , while the long intervals Ik force large local oscillations
— Ulam AI, A Note on Erdős Problem #741 (2026)
SandorA contains both B1 and B2, and their cross-sumset already equals every natural number. Enlarging the summand set cannot lose those representations, so SandorA+SandorA=Set.univ.
1. Embed B1+B2 into (B1∪B2)+(B1∪B2).
2. Embed that sumset into SandorA+SandorA.
3. Use B1+B2=Set.univ; a superset of the universe is the universe.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Quot.sound, propext what this means
Statement uses: Eq, Set, Nat, HAdd.hAdd, Erdos741.SandorA, Set.univ
Proof uses: HasSubset.Subset, Erdos741.B, Set.add_subset_add, Set.subset_union_left, Erdos741.S_C, Iff.mp, Set.univ_subset_iff, Eq.mp, congrArg, Erdos741.B_add_B_eq_univ
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma SandorA_add_SandorA_eq_univ : SandorA + SandorA = Set.univ := by
…
```
Mentions: Erdos741.SandorA
lemma Erdos741.univ_has_density_one line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.HasDensity, Nat, Set.univ, OfNat.ofNat, Real
Proof uses: GT.gt, Eq, HDiv.hDiv, Set.ncard, Inter.inter, Set, Set.Iio, Set.univ_inter, of_eq_true, Eq.trans, True, congrArg, Nat.ncard_Iio, eq_self, eq_true, True.intro, Eq.mpr, id, div_self, ne_of_gt and 4 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.univ_has_pos_density line 465 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.HasPosDensity, Nat, Set.univ
Proof uses: Exists.intro, Real, And, GT.gt, OfNat.ofNat, Set.HasDensity, And.intro, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Nat.cast_one, Eq.refl, Bool, Bool.false, Erdos741.univ_has_density_one
21 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.SandorA_has_pos_density The full sumset has natural density one line 471 source
L4DEL explanation
The key point is that B1 + B2 = N0 , while the long intervals Ik force large local oscillations
— Ulam AI, A Note on Erdős Problem #741 (2026)
Since SandorA+SandorA is Set.univ, its partial-density sequence is constantly one after the zero scale. This proves HasPosDensity in the strict sense used here: a positive natural-density limit exists.
1. Rewrite the self-sumset as Set.univ.
2. Use the theorem that the universe has density 1.
3. Package that limit with 1>0 as HasPosDensity.
Sources and attribution: Pinned Lean source (0647711a7118), Formal Conjectures density definitions, Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.HasPosDensity, Nat, HAdd.hAdd, Set, Erdos741.SandorA, Set.univ
Proof uses: Eq.mpr, id, Eq, congrArg, Erdos741.SandorA_add_SandorA_eq_univ, Erdos741.univ_has_pos_density
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma SandorA_has_pos_density : HasPosDensity (SandorA + SandorA) := by
…
```
Mentions: Erdos741.SandorA
lemma Erdos741.tendsto_Sx line 475 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Erdos741.S_x, Filter.atTop
Proof uses: Iff.mpr, Exists, LE.le, Filter.tendsto_atTop_atTop, Exists.intro, GE.ge, HPow.hPow, OfNat.ofNat, LT.lt.le, Nat.lt_pow_self, of_decide_eq_true, LT.lt, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, rfl, Decidable.byContradiction and 1 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.tendsto_Sy line 485 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Erdos741.S_y, Filter.atTop
Proof uses: Iff.mpr, Exists, LE.le, Filter.tendsto_atTop_atTop, Exists.intro, GE.ge, HPow.hPow, OfNat.ofNat, LT.lt.le, Nat.lt_pow_self, of_decide_eq_true, LT.lt, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, HMul.hMul, rfl and 2 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.finset_card_add line 495 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, GE.ge, Finset.card, HAdd.hAdd, HSub.hSub, OfNat.ofNat
Proof uses: Function.comp, Not, LT.lt, Finset.image, Finset.min', Finset.max', Inter.inter, LE.le, LE.le.trans', LE.le.trans, Union.union, Eq.ge, Finset.card_union, Finset.card_mono, of_eq_true, HasSubset.Subset, Eq.trans, True, congrArg, funext and 37 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.finset_card_add_same line 504 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, GE.ge, Finset.card, HAdd.hAdd, HSub.hSub, HMul.hMul, OfNat.ofNat
Proof uses: Function.comp, Not, LT.lt, Finset.image, Finset.min', Finset.max', Inter.inter, LE.le, LE.le.trans', LE.le.trans, Union.union, Eq.ge, Finset.card_union, Finset.card_mono, of_eq_true, HasSubset.Subset, Eq.trans, Membership.mem, True, DecidableEq and 39 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.set_add_shift_inj line 513 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Membership.mem, LE.le, GE.ge, Real, Set.ncard, Inter.inter, Set.Ico, HSub.hSub, HAdd.hAdd
Proof uses: cast, Eq.symm, Set.ncard_le_ncard_of_injOn, And.imp, Exists.intro, And, Exists, Eq, And.intro, Eq.refl, Function.comp, LT.lt, And.symm, And.rec, Decidable.byContradiction, Not, Nat.add_right_cancel, Set.toFinite
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.set_shift_size_lower_bound line 517 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, LE.le, GE.ge, Real, Set.ncard, Inter.inter, Set.Ico, HSub.hSub
Proof uses: Iff.mpr, HAdd.hAdd, sub_le_iff_le_add, cast, Eq.symm, Eq.trans, congrArg, LE.le.trans, Nat.card, Union.union, Finset, Finset.Ico, Nat.card_mono, Membership.mem, Set.ncard_union_le, Eq.le, congr_arg, Eq.rec, Finset.card, Eq and 4 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_eq_add line 521 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos741.split1, HAdd.hAdd, HMod.hMod, OfNat.ofNat, HMul.hMul, HDiv.hDiv
Proof uses: dite, Eq.mpr, id, congrArg, Not, congr, Erdos741.split1.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, Nat.zero_div, MulZeroClass.mul_zero, add_zero, Erdos741.split1.eq_1, dite_cond_eq_false, eq_false
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split2_eq_add line 526 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos741.split2, HAdd.hAdd, HSub.hSub, HMod.hMod, OfNat.ofNat, HMul.hMul, HDiv.hDiv
Proof uses: dite, Eq.mpr, id, congrArg, Not, congr, Erdos741.split2.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, tsub_self, Nat.zero_div, MulZeroClass.mul_zero, add_zero, Erdos741.split2.eq_1, dite_cond_eq_false, eq_false
36 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_eq_add' line 531 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos741.split1, HAdd.hAdd, HMod.hMod, OfNat.ofNat, HMul.hMul, HDiv.hDiv
Proof uses: dite, Eq.mpr, id, congrArg, Not, congr, Erdos741.split1.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, Nat.zero_div, MulZeroClass.mul_zero, add_zero, Erdos741.split1.eq_1, dite_cond_eq_false, eq_false
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split2_eq_add' line 539 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos741.split2, HAdd.hAdd, HSub.hSub, HMod.hMod, OfNat.ofNat, HMul.hMul, HDiv.hDiv
Proof uses: dite, Eq.mpr, id, congrArg, Not, congr, Erdos741.split2.eq_def, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self, tsub_self, Nat.zero_div, MulZeroClass.mul_zero, add_zero, Erdos741.split2.eq_1, dite_cond_eq_false, eq_false
36 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_split2_mod line 547 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, HAdd.hAdd, Erdos741.split1, Erdos741.split2, OfNat.ofNat, HSub.hSub
Proof uses: HMul.hMul, HDiv.hDiv, Erdos741.split1_eq_add', Erdos741.split2_eq_add', Decidable.byContradiction, Not, LT.lt
24 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_split2_div line 554 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, HDiv.hDiv, HAdd.hAdd, Erdos741.split1, Erdos741.split2, OfNat.ofNat
Proof uses: HMod.hMod, HMul.hMul, Erdos741.split1_eq_add', HSub.hSub, Erdos741.split2_eq_add', Decidable.byContradiction, Not, LT.lt
22 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_zero line 561 source
standard axioms: Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos741.split1, OfNat.ofNat
Proof uses: Eq.mpr, dite, Not, HAdd.hAdd, HMod.hMod, HMul.hMul, HDiv.hDiv, id, congrArg, Erdos741.split1.eq_1, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split2_zero line 565 source
standard axioms: Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos741.split2, OfNat.ofNat
Proof uses: Eq.mpr, dite, Not, HAdd.hAdd, HSub.hSub, HMod.hMod, HMul.hMul, HDiv.hDiv, id, congrArg, Erdos741.split2.eq_1, of_eq_true, Eq.trans, True, dite_cond_eq_true, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_add_base_helper line 569 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, Eq, Erdos741.split1, Erdos741.split2
Proof uses: Nat.strongRecOn, LT.lt, dite, And, OfNat.ofNat, Eq.mpr, id, congrArg, Erdos741.split1_zero, Erdos741.split2_zero, add_zero, Eq.refl, Eq.symm, Not, HMod.hMod, HSub.hSub, Erdos741.split1_split2_mod, HDiv.hDiv, Erdos741.split1_split2_div, HMul.hMul and 3 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_split2_add_split1 line 590 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos741.split1, HAdd.hAdd, Erdos741.split2
Proof uses: Erdos741.split1_add_base_helper, Decidable.byContradiction, LE.le, Not
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split2_add_base_helper line 593 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, Eq, Erdos741.split2, Erdos741.split1
Proof uses: Nat.strongRecOn, LT.lt, dite, And, OfNat.ofNat, Eq.mpr, id, congrArg, Erdos741.split1_zero, Erdos741.split2_zero, add_zero, Eq.refl, Eq.symm, Not, HMod.hMod, HSub.hSub, Erdos741.split1_split2_mod, HDiv.hDiv, Erdos741.split1_split2_div, HMul.hMul and 3 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_split2_add_split2 line 614 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos741.split2, HAdd.hAdd, Erdos741.split1
Proof uses: Erdos741.split2_add_base_helper, Decidable.byContradiction, LE.le, Not
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split1_add_base line 617 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Erdos741.B1, Erdos741.B2, Eq, Erdos741.split1, HAdd.hAdd
Proof uses: Erdos741.split2, Erdos741.split1_split2_add_split1
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.split2_add_base line 622 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Erdos741.B1, Erdos741.B2, Eq, Erdos741.split2, HAdd.hAdd
Proof uses: Erdos741.split1, Erdos741.split1_split2_add_split2
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.cross_term_disjoint line 627 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Disjoint, HAdd.hAdd, Inter.inter, Erdos741.B1, Erdos741.B2
Proof uses: Eq.mpr, Eq, EmptyCollection.emptyCollection, id, congrArg, propext, Set.disjoint_iff_inter_eq_empty, Set.ext, Iff, Membership.mem, Exists, And, Not, Eq.trans, False, congr, funext, iff_false, Erdos741.split1, Eq.symm and 4 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.sum_size_bound line 653 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, LE.le, Set.ncard, Inter.inter, HAdd.hAdd, Set.Iio, HMul.hMul
Proof uses: HasSubset.Subset, Set.image, Prod, Prod.fst, Prod.snd, SProd.sprod, Membership.mem, And, Exists, Eq, And.left, Exists.intro, Prod.mk, LT.lt, And.right, Decidable.byContradiction, Not, And.intro, rfl, Set.Finite and 8 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.uv_bound_algebra line 668 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, HMul.hMul, HSub.hSub, OfNat.ofNat, HAdd.hAdd
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_left and 42 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.density_le_one line 680 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real, Set.HasDensity, Set.univ, LE.le, OfNat.ofNat
Proof uses: le_of_tendsto', HMul.hMul, Set.ncard, Inter.inter, Set.Iio, Inv.inv, Filter.atTop, Eq.mp, Filter.Tendsto, Set.partialDensity, nhds, congrArg, HDiv.hDiv, funext, div_eq_mul_inv, div_le_one_of_le₀, cast, Eq.symm, Nat.card_mono, And.imp_left and 3 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.density_ge_zero line 684 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real, Set.HasDensity, Set.univ, GE.ge, OfNat.ofNat
Proof uses: id, ge_of_tendsto', Set.partialDensity, Filter.atTop, div_nonneg, Set.ncard, Inter.inter, Set.Iio, Nat.cast_nonneg
59 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.sum_size_bound_eps line 688 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, LE.le, Real, Set.ncard, Inter.inter, HAdd.hAdd, Set.Iio, HMul.hMul
Proof uses: Erdos741.sum_size_bound, cast, Eq.symm, Eq.trans, congrArg
41 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_B2_cross_bound line 693 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Real, HMul.hMul, LE.le, HDiv.hDiv, Set.ncard, Inter.inter, HAdd.hAdd, Erdos741.B1, Erdos741.B2, Set.Iio
Proof uses: Erdos741.sum_size_bound_eps, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Inv.inv, OfNat.ofNat, Mathlib.Tactic.Ring.div_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_left, Mathlib.Tactic.Ring.mul_pf_right, Mathlib.Tactic.Ring.one_mul, Mathlib.Tactic.Ring.mul_zero, Mathlib.Tactic.Ring.add_pf_add_zero and 61 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.Sx_eq_sq line 702 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Erdos741.S_x, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: rfl, Trans.trans, Eq.mpr, id, congrArg, Eq.refl, mul_pow, congr, Eq.trans, Nat.cast_mul, Nat.cast_pow
36 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.Mk_pos line 710 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, Real, HPow.hPow, OfNat.ofNat
Proof uses: pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Erdos741.base2_to_base4 line 712 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, Eq, OfNat.ofNat, Not, HAdd.hAdd, HMod.hMod, HMul.hMul, HDiv.hDiv
12 instances, coercions and auxiliary constants left out.
lemma Erdos741.base2_to_base4_lt_4_pow line 716 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, LT.lt, Erdos741.base2_to_base4, HPow.hPow, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, id, Eq, congrArg, Eq.symm, Nat.mul_pow, Eq.refl, dite, Not, HAdd.hAdd, HMod.hMod, HDiv.hDiv, Erdos741.base2_to_base4.eq_1, Erdos741.base2_to_base4_lt_4_pow.match_2, WellFounded.Nat.fix, InvImage, Unit, of_eq_true, Eq.trans and 41 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
def Erdos741.extract_binary line 724 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, Eq, OfNat.ofNat, Not, HAdd.hAdd, HMod.hMod, HMul.hMul, HDiv.hDiv
12 instances, coercions and auxiliary constants left out.
lemma Erdos741.split1_eq_base2_to_base4 line 728 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos741.split1, Erdos741.base2_to_base4, Erdos741.extract_binary
Proof uses: id, Nat.strongRec, WellFounded.Nat.fix, InvImage, LT.lt, dite, OfNat.ofNat, Not, HAdd.hAdd, HMod.hMod, HMul.hMul, HDiv.hDiv, Even, Odd, Or, Nat.even_or_odd, Ne, eq_or_ne, HEq, Eq.refl and 48 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_subset_base2_to_base4 line 741 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Erdos741.B1, Exists, Eq, Erdos741.base2_to_base4
Proof uses: Erdos741.split1, Exists.intro, Erdos741.extract_binary, Eq.mpr, id, congrArg, Erdos741.split1_eq_base2_to_base4, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_Iio_bound line 746 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Set.ncard, Inter.inter, Set, Erdos741.B1, Set.Iio, HPow.hPow, OfNat.ofNat
Proof uses: HasSubset.Subset, Set.image, Erdos741.base2_to_base4, Membership.mem, Eq, Exists, Erdos741.B1_subset_base2_to_base4, And.left, Exists.intro, And, LT.lt, Eq.mpr, id, congrArg, Eq.symm, And.right, And.intro, Iff.mp, Erdos741.base2_to_base4_lt_4_pow, Set.Finite and 13 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B2_eq_2_B1 line 762 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Erdos741.B2, Exists, And, Erdos741.B1, Eq, HMul.hMul, OfNat.ofNat
Proof uses: Erdos741.split2, Exists.intro, Erdos741.split1, HDiv.hDiv, And.intro, rfl, Erdos741.split2_eq_two_mul_split1
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B2_Iio_bound line 767 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Set.ncard, Inter.inter, Set, Erdos741.B2, Set.Iio, HPow.hPow, OfNat.ofNat
Proof uses: HasSubset.Subset, Set.image, HMul.hMul, Erdos741.B1, Membership.mem, And, Eq, Exists, Erdos741.B2_eq_2_B1, And.left, Exists.intro, LT.lt, And.right, Decidable.byContradiction, Not, And.intro, rfl, Eq.symm, Set.Finite, Set.Finite.subset and 6 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def Erdos741.x_seq line 782 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real
Proof uses: HDiv.hDiv, Set.ncard, Inter.inter, Erdos741.B1, Set.Iio, Erdos741.S_x, HPow.hPow, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
def Erdos741.y_seq line 783 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real
Proof uses: HDiv.hDiv, Set.ncard, Inter.inter, Erdos741.B2, Set.Iio, Erdos741.S_x, HPow.hPow, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
lemma Erdos741.x_seq_bounds line 785 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, And, LE.le, Real, OfNat.ofNat, Erdos741.x_seq
Proof uses: And.intro, div_nonneg, Set.ncard, Inter.inter, Erdos741.B1, Set.Iio, Erdos741.S_x, HPow.hPow, Nat.cast_nonneg, le_of_lt, Iff.mpr, LT.lt, Nat.cast_pos', pow_pos, inferInstance, PartialOrder, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool and 21 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.y_seq_bounds line 803 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, And, LE.le, Real, OfNat.ofNat, Erdos741.y_seq
Proof uses: And.intro, div_nonneg, Set.ncard, Inter.inter, Erdos741.B2, Set.Iio, Erdos741.S_x, HPow.hPow, Nat.cast_nonneg, le_of_lt, Iff.mpr, LT.lt, Nat.cast_pos', pow_pos, inferInstance, PartialOrder, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool and 21 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A1_cross_bound line 821 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, LE.le, Real, HDiv.hDiv, Set.ncard, Inter.inter, HAdd.hAdd, Erdos741.B1, Erdos741.B2, Set.Iio, Erdos741.S_x, HMul.hMul, Erdos741.x_seq, Erdos741.y_seq
Proof uses: Eq, HPow.hPow, OfNat.ofNat, Erdos741.Sx_eq_sq, Erdos741.B1_B2_cross_bound
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B1_sum_Iio_bound line 827 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Set.ncard, Inter.inter, Set, HAdd.hAdd, Erdos741.B1, Set.Iio, Erdos741.S_x, HPow.hPow, OfNat.ofNat
Proof uses: Eq, rfl, Erdos741.B1_sum_ncard, Eq.mpr, id, congrArg, cast, Eq.symm, Eq.trans
52 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B2_sum_Iio_bound line 833 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Set.ncard, Inter.inter, Set, HAdd.hAdd, Erdos741.B2, Set.Iio, Erdos741.S_x, HPow.hPow, OfNat.ofNat
Proof uses: Eq, rfl, Erdos741.B2_sum_ncard, Eq.mpr, id, congrArg, cast, Eq.symm, Eq.trans
52 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.SC_Iio_bound line 839 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Real, Set.ncard, Inter.inter, Set, Erdos741.S_C, Set.Iio, Erdos741.S_x, Erdos741.S_y, HSub.hSub
Proof uses: id, Function.comp, Nat.card, Finset, Finset.biUnion, Finset.range, Finset.Ico, HPow.hPow, HMul.hMul, Set.iUnion, Set.Ico, Iff.mpr, Nat.cast_le, LE.le.trans, Nat.card_mono, Finset.finite_toSet, Membership.mem, And, Exists, Finset.mem_biUnion and 129 more
156 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.SC_sum_bound line 845 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Real, Set.ncard, Inter.inter, Set, HAdd.hAdd, Erdos741.S_C, Set.Iio, Erdos741.S_x, HMul.hMul, Erdos741.S_y, HSub.hSub
Proof uses: Erdos741.sum_size_bound_eps, Erdos741.SC_Iio_bound, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add and 39 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B_Iio_bound line 850 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Set.ncard, Inter.inter, Set, Erdos741.B, Set.Iio, Erdos741.S_x, HMul.hMul, OfNat.ofNat, HPow.hPow
Proof uses: Eq, rfl, Eq.mpr, id, congrArg, HasSubset.Subset, Union.union, Erdos741.B1, Erdos741.B2, Membership.mem, Or.inl, And.intro, Or.inr, Set.Finite, Set.Finite.subset, Set.finite_Iio, Set.inter_subset_right, HAdd.hAdd, Set.ncard_union_le, Trans.trans and 66 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.SC_B_bound line 871 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Real, Set.ncard, Inter.inter, Set, HAdd.hAdd, Erdos741.S_C, Erdos741.B, Set.Iio, Erdos741.S_x, HMul.hMul, Erdos741.S_y, HSub.hSub, HPow.hPow
Proof uses: Erdos741.sum_size_bound_eps, Erdos741.SC_Iio_bound, Erdos741.B_Iio_bound, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add and 44 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.ncard_union_le_6 line 877 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, LE.le, Real, Set.ncard, Union.union, HAdd.hAdd
Proof uses: cast, Nat, Eq.symm, Eq.trans, congrArg, LE.le.trans, Set.ncard_union_le, Nat.add_le_add_right, refl
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A1_subset_SandorA line 880 source
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, HasSubset.Subset, Erdos741.B1, Erdos741.B2, Erdos741.S_C
Proof uses: Membership.mem, Eq.mpr, id, congrArg, Or.inl, Erdos741.B, Or.inr
5 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A1_sum_subset line 891 source
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, HasSubset.Subset, Inter.inter, HAdd.hAdd, Set.Iio, Erdos741.S_x, Erdos741.B1, Erdos741.B2, Erdos741.B, Erdos741.S_C
Proof uses: Membership.mem, And, Exists, Erdos741.A1_subset_SandorA, Or.inl, Or.inr, And.intro, Exists.intro, rfl, Nat.add_comm
18 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B_SC_comm line 911 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, Set.ncard, Inter.inter, Set, HAdd.hAdd, Erdos741.B, Erdos741.S_C, Set.Iio, Erdos741.S_x
Proof uses: add_comm, Eq.mpr, id, congrArg, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A1_sum_decomp_bound line 915 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, GE.ge, OfNat.ofNat, LE.le, Real, Set.ncard, Inter.inter, HAdd.hAdd, Set.Iio, Erdos741.S_x, Erdos741.B1, Erdos741.B2, HMul.hMul, Erdos741.S_C, Erdos741.B
Proof uses: HasSubset.Subset, Erdos741.A1_sum_subset, Set.Finite, Set.Finite.subset, Set.finite_Iio, Membership.mem, Or, And, LT.lt, Eq.mp, Eq.trans, congr, congrArg, Set.ncard_le_ncard, Erdos741.ncard_union_le_6, Erdos741.B_SC_comm, cast, Eq.symm, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl and 51 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A1_density_drop line 934 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, GE.ge, OfNat.ofNat, LE.le, Real, HDiv.hDiv, Set.ncard, Inter.inter, HAdd.hAdd, Set.Iio, Erdos741.S_x, HMul.hMul, Erdos741.x_seq, Erdos741.y_seq, HPow.hPow, Erdos741.S_y and 1 more
Proof uses: Erdos741.B1, Erdos741.B2, Erdos741.S_C, Erdos741.B, Erdos741.A1_sum_decomp_bound, Erdos741.A1_cross_bound, Erdos741.B1_sum_Iio_bound, Erdos741.B2_sum_Iio_bound, Erdos741.SC_B_bound, Erdos741.SC_sum_bound, GT.gt, rfl, Trans.trans, Eq.mpr, id, congrArg, Eq.trans, Eq.refl, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat and 73 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A2_sum_subset line 958 source
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, HasSubset.Subset, Inter.inter, HAdd.hAdd, Set.Iio, Erdos741.S_x, Erdos741.B1, Erdos741.B2, Erdos741.B, Erdos741.S_C
Proof uses: Membership.mem, And, Exists, Erdos741.A1_subset_SandorA, Eq.mpr, id, congrArg, Set.union_comm, Eq.refl, Or.inl, Or.inr, And.intro, Exists.intro, rfl, Nat.add_comm
18 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A2_sum_decomp_bound line 978 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, GE.ge, OfNat.ofNat, LE.le, Real, Set.ncard, Inter.inter, HAdd.hAdd, Set.Iio, Erdos741.S_x, Erdos741.B1, Erdos741.B2, HMul.hMul, Erdos741.S_C, Erdos741.B
Proof uses: HasSubset.Subset, Erdos741.A2_sum_subset, Set.Finite, Set.Finite.subset, Set.finite_Iio, Membership.mem, Or, And, LT.lt, Eq.mp, Eq.trans, congr, congrArg, Set.ncard_le_ncard, Erdos741.ncard_union_le_6, Erdos741.B_SC_comm, cast, Eq.symm, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl and 51 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A2_B1_bound line 997 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, LE.le, Real, HDiv.hDiv, Set.ncard, Inter.inter, Erdos741.B1, Set.Iio, Erdos741.S_x, HPow.hPow, OfNat.ofNat, HSub.hSub, Erdos741.x_seq
Proof uses: Disjoint.mono, Membership.mem, And.left, Set.ext, Eq.mpr, Iff, Or, And, LT.lt, id, congr, congrArg, Eq.trans, Iff.intro, And.intro, Or.inl, Erdos741.B, Erdos741.S_C, Erdos741.B2, Eq.mp and 92 more
174 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A2_B2_bound line 1032 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, LE.le, Real, HDiv.hDiv, Set.ncard, Inter.inter, Erdos741.B2, Set.Iio, Erdos741.S_x, HPow.hPow, OfNat.ofNat, HSub.hSub, Erdos741.y_seq
Proof uses: Disjoint.mono, Membership.mem, And.left, Set.ext, Eq.mpr, Iff, Or, And, LT.lt, id, congr, congrArg, Eq.trans, Iff.intro, And.intro, Or.inl, Erdos741.B, Erdos741.S_C, Or.inr, Erdos741.B1 and 92 more
174 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A2_cross_bound line 1067 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, LE.le, Real, HDiv.hDiv, Set.ncard, Inter.inter, HAdd.hAdd, Erdos741.B1, Erdos741.B2, Set.Iio, Erdos741.S_x, HMul.hMul, HSub.hSub, OfNat.ofNat, Erdos741.x_seq and 1 more
Proof uses: HPow.hPow, Erdos741.Sx_eq_sq, Erdos741.B1_B2_cross_bound, Erdos741.A2_B1_bound, Erdos741.A2_B2_bound, Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos, Nat.cast_nonneg', Iff.mpr, LT.lt, Nat.cast_pos', pow_pos, inferInstance, PartialOrder, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, mul_le_mul, le_of_not_gt and 72 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.A2_density_drop line 1077 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, GE.ge, OfNat.ofNat, LE.le, Real, HDiv.hDiv, Set.ncard, Inter.inter, HAdd.hAdd, Set.Iio, Erdos741.S_x, HMul.hMul, HSub.hSub, Erdos741.x_seq, Erdos741.y_seq and 2 more
Proof uses: Erdos741.B1, Erdos741.B2, Erdos741.S_C, Erdos741.B, Erdos741.A2_sum_decomp_bound, Erdos741.A2_cross_bound, Erdos741.B1_sum_Iio_bound, Erdos741.B2_sum_Iio_bound, Erdos741.SC_B_bound, Erdos741.SC_sum_bound, GT.gt, rfl, Trans.trans, Eq.mpr, id, congrArg, Eq.trans, Eq.refl, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat and 75 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.error_term_tendsto line 1101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow, Erdos741.S_y, HSub.hSub, Erdos741.S_x, Filter.atTop, nhds
Proof uses: id, Iff.mp, Filter.tendsto_add_atTop_iff_nat, Eq.mpr, Mathlib.Meta.NormNum.instAtLeastTwo, Eq, Eq.trans, congrArg, funext, congr, pow_succ', pow_mul, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1, add_tsub_cancel_right, Nat.cast_mul and 56 more
175 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.error_term_le_eps line 1107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, Nat, GE.ge, LE.le, HDiv.hDiv, HAdd.hAdd, HMul.hMul, HPow.hPow, Erdos741.S_y, HSub.hSub, Erdos741.S_x
Proof uses: Membership.mem, Set, Filter, nhds, Set.Iio, Iio_mem_nhds, Filter.map, Filter.atTop, Erdos741.error_term_tendsto, Iff.mp, Filter.Eventually, Filter.eventually_atTop, Exists.intro, le_of_lt
78 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.partialDensity_eq line 1117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Real, Set.partialDensity, Set.univ, HDiv.hDiv, Set.ncard, Inter.inter, Set.Iio
Proof uses: of_eq_true, Eq.trans, Finset.card, Finset.filter, Membership.mem, Finset.Iio, True, congr, congrArg, Set.toFinset, Set.inter_comm, Set.univ_inter, Set.ncard_eq_toFinset_card', Fintype.card, Set.toFinset_card, Fintype.ofFinset, Fintype.card_ofFinset, Finset, Finset.filter.congr_simp, Eq.refl and 3 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.limit_lower_bound_A line 1119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real, Set.HasDensity, Set.univ, GT.gt, OfNat.ofNat, Exists, GE.ge, HDiv.hDiv, Set.ncard, Inter.inter, Set.Iio, HSub.hSub
Proof uses: Membership.mem, Filter, nhds, Set.Ioi, Ioi_mem_nhds, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat and 43 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.limit_exists_eps line 1132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, Real, Set.HasDensity, HAdd.hAdd, Set.univ, GT.gt, OfNat.ofNat, Exists, And, LE.le, HMul.hMul, HSub.hSub
Proof uses: HDiv.hDiv, id, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat and 119 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B_partition_alpha_bound_eps line 1173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, Real, Set.HasDensity, HAdd.hAdd, Set.univ, GT.gt, OfNat.ofNat, LE.le, HSub.hSub, HMul.hMul
Proof uses: GE.ge, Erdos741.density_ge_zero, Erdos741.density_le_one, Exists, And, Exists.intro, HDiv.hDiv, And.intro, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HPow.hPow, Nat.rawCast and 80 more
149 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B_partition_alpha_bound Any convergent two-colour split pays a cross-term density deficit line 1199 source
L4DEL explanation
Taking k → ∞ yields
— Ulam AI, A Note on Erdős Problem #741 (2026)
If the two monochromatic self-sumsets have natural-density limits α₁ and α₂, then the carry-free digit split forces α₁+α₂ ≤ 1-α₁α₂. In particular, if both limits are positive, their sum is uniformly below one.
1. Inspect each colour's proportions inside the B1 and B2 digit sets at the lower scales.
2. Bound pure-colour self-sums by the matching products of those proportions; mixed digit sums occupy the missing cross term.
3. Pass to the assumed limits and remove an arbitrary epsilon to obtain the exact inequality.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, Real, Set.HasDensity, HAdd.hAdd, Set.univ, LE.le, HSub.hSub, OfNat.ofNat, HMul.hMul
Proof uses: Inter.inter, Erdos741.B1, Erdos741.B2, Erdos741.cross_term_disjoint, le_of_forall_pos_le_add, LT.lt, Erdos741.B_partition_alpha_bound_eps
90 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma B_partition_alpha_bound (A₁ A₂ : Set ℕ) (h_union : SandorA = A₁ ∪ A₂) (h_disj : Disjoint A₁ A₂)
  (α₁ α₂ : ℝ) (h_dens1 : HasDensity (A₁ + A₁) α₁) (h_dens2 : HasDensity (A₂ + A₂) α₂) :
  α₁ + α₂ ≤ 1 - α₁ * α₂ := by
…
```
Mentions: Erdos741.SandorA
lemma Erdos741.alpha_sum_bound line 1207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, Real, Set.HasDensity, HAdd.hAdd, Set.univ, GT.gt, OfNat.ofNat, LT.lt
Proof uses: LE.le, HSub.hSub, HMul.hMul, Erdos741.B_partition_alpha_bound, mul_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt and 38 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.limit_upper_bound line 1214 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real, Set.HasDensity, Set.univ, GT.gt, OfNat.ofNat, Exists, GE.ge, LT.lt, HDiv.hDiv, Set.ncard, Inter.inter, Set.Iio, HAdd.hAdd
Proof uses: Membership.mem, Filter, nhds, Iio_mem_nhds, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_zero and 40 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.limit_lower_bound line 1227 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real, Set.HasDensity, Set.univ, GT.gt, OfNat.ofNat, Exists, GE.ge, HDiv.hDiv, Set.ncard, Inter.inter, Set.Iio, HSub.hSub
Proof uses: Membership.mem, Filter, nhds, Set.Ioi, Ioi_mem_nhds, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat and 43 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.tendsto_2Sx line 1242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, HMul.hMul, OfNat.ofNat, Erdos741.S_x, Filter.atTop
Proof uses: Erdos741.tendsto_Sx, Filter.tendsto_atTop_mono, Decidable.byContradiction, LE.le, Not
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.tendsto_2Sy line 1246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter.Tendsto, Nat, HMul.hMul, OfNat.ofNat, Erdos741.S_y, Filter.atTop
Proof uses: Erdos741.tendsto_Sy, Filter.tendsto_atTop_mono, Decidable.byContradiction, LE.le, Not
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.B_partition_density line 1250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, Real, Set.HasDensity, HAdd.hAdd, Set.univ, GT.gt, OfNat.ofNat, Exists, And, GE.ge, LE.le, HDiv.hDiv, Set.ncard, Inter.inter, Set.Iio and 3 more
Proof uses: Exists.intro, div_pos, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, And.intro, LT.lt, Erdos741.limit_upper_bound, Filter.Tendsto, Filter.atTop, Erdos741.tendsto_2Sx, Max.max, Iff.mp, Filter.tendsto_atTop_atTop, le_trans, le_max_left and 90 more
165 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.set_card_add_same_general line 1281 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Set.Finite, GE.ge, Real, Set.ncard, HAdd.hAdd, HSub.hSub, HMul.hMul, OfNat.ofNat
Proof uses: Iff.mpr, LE.le, sub_le_iff_le_add, Exists.elim, Finset, Eq, Set.Finite.exists_finset_coe, Eq.rec, cast, Finset.card, Eq.symm, Eq.trans, congrArg, Nat.cast_one, congr, Set.ncard_coe_finset, Or.elim, EmptyCollection.emptyCollection, Finset.Nonempty, Finset.eq_empty_or_nonempty and 108 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.sandor_cross_sums A fat interval forces almost twice its size in monochromatic sums line 1291 source
L4DEL explanation
Propositions 3.3 and 3.4 would give the contradiction
— Ulam AI, A Note on Erdős Problem #741 (2026)
Partition the interval [S_x(k),S_y(k)) between two colours. For each colour, a finite nonempty set U satisfies |U+U|≥2|U|-1; adding the two bounds yields at least 2*(S_y-S_x)-2 same-colour sums in the doubled interval.
1. Intersect each colour with the whole fat interval; the two intersections partition it.
2. Apply the elementary sumset lower bound separately to both pieces.
3. Add the bounds and place all resulting sums between 2*S_x(k) and 2*S_y(k).
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, GE.ge, OfNat.ofNat, Real, HAdd.hAdd, Set.ncard, Inter.inter, Set.Ico, HMul.hMul, Erdos741.S_x, Erdos741.S_y, HSub.hSub
Proof uses: HasSubset.Subset, Membership.mem, Or.inr, Erdos741.B, Erdos741.S_C, Set.mem_iUnion_of_mem, Eq.mpr, id, congrArg, Eq.symm, Set.ncard_union_eq, Disjoint.mono, Set.inter_subset_left, Set.union_inter_distrib_right, Iff.mpr, Set.inter_eq_right, Eq.refl, cast, Eq.trans, HPow.hPow and 159 more
217 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma sandor_cross_sums (A₁ A₂ : Set ℕ) (h_union : SandorA = A₁ ∪ A₂) (h_disj : Disjoint A₁ A₂) (k : ℕ) (hk : k ≥ 10) :
  (((A₁ + A₁) ∩ Ico (2 * S_x k) (2 * S_y k)).ncard : ℝ) + (((A₂ + A₂) ∩ Ico (2 * S_x k) (2 * S_y k)).ncard : ℝ)
    ≥ 2 * ((S_y k : ℝ) - (S_x k : ℝ)) - 2 := by
…
```
Mentions: Erdos741.SandorA, Erdos741.S_x, Erdos741.S_y
lemma Erdos741.exists_K1_cx line 1326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, Nat, GE.ge, HMul.hMul, Erdos741.S_x
Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo and 67 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.algebra_fluctuation line 1335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Eq, HMul.hMul, Nat, GE.ge, LE.le, HSub.hSub, HDiv.hDiv, HAdd.hAdd
Proof uses: lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_zero, Nat.cast_zero and 89 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.SandorA_fluctuation_bounds Positive limiting densities would still oscillate by a fixed amount line 1359 source
L4DEL explanation
Propositions 3.3 and 3.4 would give the contradiction
— Ulam AI, A Note on Erdős Problem #741 (2026)
Assuming both monochromatic self-sumsets have positive natural-density limits, this lemma constructs lower checkpoints N(k)=2*S_x(k) and upper checkpoints M(k)=2*S_y(k) where their combined partial density at M(k) exceeds that at N(k) by one fixed delta>0 forever.
1. Positivity and the partition bound give a fixed deficit below one at the lower checkpoints.
2. The fat interval contributes enough new same-colour sums to recover more than that deficit at the upper checkpoints.
3. Both checkpoint sequences tend to infinity, so the permanent gap is incompatible with convergence to α₁+α₂.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, Real, Set.HasDensity, HAdd.hAdd, Set.univ, GT.gt, OfNat.ofNat, Exists, And, Filter.Tendsto, Filter.atTop, GE.ge, HDiv.hDiv, Set.ncard, Inter.inter and 1 more
Proof uses: LE.le, HMul.hMul, Erdos741.S_x, HSub.hSub, Erdos741.B_partition_density, Erdos741.exists_K1_cx, Exists.intro, Erdos741.S_y, Max.max, div_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, And.intro, Erdos741.tendsto_2Sy, Erdos741.tendsto_2Sx and 149 more
226 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma SandorA_fluctuation_bounds (A₁ A₂ : Set ℕ) (h_union : SandorA = A₁ ∪ A₂) (h_disj : Disjoint A₁ A₂)
  (α₁ α₂ : ℝ) (h_dens1 : HasDensity (A₁ + A₁) α₁) (h_dens2 : HasDensity (A₂ + A₂) α₂) (h_pos1 : α₁ > 0) (h_pos2 : α₂ > 0) :
  ∃ (M N : ℕ → ℕ) (K0 : ℕ) (delta : ℝ), delta > 0 ∧ Filter.Tendsto M Filter.atTop Filter.atTop ∧ Filter.Tendsto N Filter.atTop Filter.atTop ∧
  ∀ k ≥ K0, (((A₁ + A₁) ∩ Iio (M k)).ncard : ℝ) / (M k : ℝ) + (((A₂ + A₂) ∩ Iio (M k)).ncard : ℝ) / (M k : ℝ)
     ≥ (((A₁ + A₁) ∩ Iio (N k)).ncard : ℝ) / (N k : ℝ) + (((A₂ + A₂) ∩ Iio (N k)).ncard : ℝ) / (N k : ℝ) + delta := by
…
```
Mentions: Erdos741.SandorA
lemma Erdos741.max_of_five line 1414 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Exists, And, GE.ge
Proof uses: Exists.intro, Max.max, Decidable.byContradiction, Not, And.intro
9 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.tendsto_ge_max line 1423 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Filter.Tendsto, Filter.atTop, Exists, And, GE.ge
Proof uses: LE.le, Iff.mp, Filter.tendsto_atTop_atTop, Exists.intro, Max.max, And.intro, Decidable.byContradiction, Not
21 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.has_pos_density_nonempty line 1437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real, Set.HasDensity, HAdd.hAdd, Set.univ, GT.gt, OfNat.ofNat, Set.Nonempty
Proof uses: Decidable.byContradiction, Not, Eq, EmptyCollection.emptyCollection, Eq.mpr, id, congrArg, Eq.mp, propext, Set.not_nonempty_iff_eq_empty, of_eq_true, Eq.trans, True, Set.add_empty, eq_self, LE.le, False.elim, LT.lt, False, Filter.Tendsto and 53 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Erdos741.SandorA_no_valid_partition No disjoint two-part split can give both self-sumsets positive natural density line 1447 source
L4DEL explanation
Propositions 3.3 and 3.4 would give the contradiction
— Ulam AI, A Note on Erdős Problem #741 (2026)
Suppose both component self-sumsets had positive limits. Convergence would make each combined partial density arbitrarily close to α₁+α₂ at every sufficiently large scale, but SandorA_fluctuation_bounds produces two arbitrarily large scales separated by a fixed positive gap.
1. Unpack the two HasPosDensity hypotheses into positive limits and convergence proofs.
2. Choose upper and lower convergence bounds with tolerance delta/4 for both colours.
3. Evaluate at a sufficiently large fluctuation checkpoint and derive the numerical contradiction.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Eq, Erdos741.SandorA, Union.union, Disjoint, Not, And, Set.HasPosDensity, HAdd.hAdd, Set.univ
Proof uses: False, Real, GT.gt, OfNat.ofNat, Set.HasDensity, Exists, Filter.Tendsto, Filter.atTop, GE.ge, HDiv.hDiv, Set.ncard, Inter.inter, Set.Iio, Erdos741.SandorA_fluctuation_bounds, div_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo and 90 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma SandorA_no_valid_partition :
  ∀ A₁ A₂, SandorA = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬(HasPosDensity (A₁ + A₁) ∧ HasPosDensity (A₂ + A₂)) := by
…
```
Mentions: Erdos741.SandorA
lemma Erdos741.exists_erdos_counterexample The explicit witness refuting the strict-natural-density statement line 1480 source
L4DEL explanation
For ordinary natural density, the first question has a negative answer. For upper density, the first question has a positive answer.
— Ulam AI, A Note on Erdős Problem #741 (2026)
SandorA has a self-sumset of natural density one, yet every disjoint two-part split fails to give positive natural-density limits to both component self-sumsets. This is the witness needed to negate the universal strict-density version of Erdős 741(i).
1. Use SandorA as the existential set.
2. Supply SandorA_has_pos_density for its full self-sumset.
3. Supply SandorA_no_valid_partition for every proposed partition.
Sources and attribution: Pinned Lean source (0647711a7118), Ulam AI, A Note on Erdős Problem #741 (2026)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Set, Nat, And, Set.HasPosDensity, HAdd.hAdd, Set.univ, Eq, Union.union, Disjoint, Not
Proof uses: Exists.intro, Erdos741.SandorA, And.intro, Erdos741.SandorA_has_pos_density, Erdos741.SandorA_no_valid_partition
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma exists_erdos_counterexample : ∃ A : Set ℕ, HasPosDensity (A + A) ∧ ∀ A₁ A₂, A = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬ (HasPosDensity (A₁ + A₁) ∧ HasPosDensity (A₂ + A₂)) := by
…
```
theorem Erdos741.target_theorem_0 Erdős problem 741(i): strict natural density is false, upper density is true line 1486 source
L4DEL explanation
We show that the answer is yes. We use an alternating block partition.
— Human-written proof companion for Erdős 741(i)
For ordinary natural density, the first question has a negative answer. For upper density, the first question has a positive answer.
— Ulam AI, A Note on Erdős Problem #741 (2026)
Can one always decompose the sequence A as the union of two disjoint subsequences
— Paul Erdős, Some of my favourite problems which recently have been solved (1994), p. 263
This Lean theorem proves answer(False) for HasPosDensity, which here means that a positive ordinary natural-density limit exists. The pinned companion proves a different, compatible theorem for positive upper density. The two artifacts do not disagree: density choice changes the answer. The lower-density variant is separate and remains unresolved in the cited status sources.
1. The Lean development builds SandorA, whose full self-sumset is all naturals and therefore has natural density one.
2. Its carry-free digit sets make monochromatic self-sums sparse at lower checkpoints, while added fixed-factor fat intervals force many such sums at upper checkpoints.
3. Any partition with two positive natural-density limits would therefore oscillate by a fixed amount, contradicting convergence; this supplies the negative witness.
4. The companion's alternating-block argument concerns upper density, where only a positive limsup is required, so it supports the separate affirmative variant and does not explain this Lean proof.
Sources and attribution: Pinned Lean source (0647711a7118), Human-written proof companion for Erdős 741(i), Pinned AlphaProof Lean result for Erdős 741(i), Formal Conjectures density definitions, Ulam AI, A Note on Erdős Problem #741 (2026), Paul Erdős, Some of my favourite problems which recently have been solved (1994), p. 263, Erdős Problems 741 current status record
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, Set, Nat, Set.HasPosDensity, HAdd.hAdd, Set.univ, Exists, And, Eq, Union.union, Disjoint
Proof uses: Iff.intro, False.elim, Not, Erdos741.exists_erdos_counterexample, And.intro
36 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: APNOutputs/ErdosProblems/erdos_741.parts.ii.lean:634 (different declaration text). Qualify references as Erdos741.target_theorem_0@path.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem target_theorem_0
  : answer(
  -- EVOLVE-VALUE-START
  False
  -- EVOLVE-VALUE-END
  ) ↔ ∀ A : Set ℕ, HasPosDensity (A + A) → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ HasPosDensity (A₁ + A₁) ∧ HasPosDensity (A₂ + A₂) := by
…
```