noncomputable def Finset.ABCExceptionsBelow (μ : ℝ) (X : ℕ) : Finset (ℕ × ℕ × ℕ)

The set (as a Finset) of exceptions to the ABC conjecture at μ inside [1, X] ^ 3, in particular the set of triples (a, b, c) which are

• pairwise coprime,
• contained in [1, X] ^ 3,
• satisfy a + b = c,
• have radical (a * b * c) < c ^ μ

Note this has a slight difference from the usual formulation, which has radical (a * b * c) ^ (1 + ε) < c instead.

@[simp]

theorem Finset.mem_ABCExceptionsBelow (μ : ℝ) (X a b c : ℕ) : (a, b, c) ∈ ABCExceptionsBelow μ X ↔ a.Coprime b ∧ a.Coprime c ∧ b.Coprime c ∧ a + b = c ∧ ↑(UniqueFactorizationMonoid.radical (a * b * c)) < ↑c ^ μ ∧ (a, b, c) ∈ Set.Icc (1, 1, 1) (X, X, X)

def Set.ABCExceptionsBelow (μ : ℝ) (X : ℕ) : Set (ℕ × ℕ × ℕ)

The set of exceptions to the ABC conjecture at μ inside [1, X] ^ 3, in particular the set of triples (a, b, c) which are

• pairwise coprime,
• contained in [1, X] ^ 3,
• satisfy a + b = c,
• have radical (a * b * c) < c ^ μ

Note this has a slight difference from the usual formulation, which has radical (a * b * c) ^ (1 + ε) < c instead.

@[simp]

theorem Set.mem_ABCExceptionsBelow (μ : ℝ) (X a b c : ℕ) : (a, b, c) ∈ ABCExceptionsBelow μ X ↔ a.Coprime b ∧ a.Coprime c ∧ b.Coprime c ∧ a + b = c ∧ ↑(UniqueFactorizationMonoid.radical (a * b * c)) < ↑c ^ μ ∧ (a, b, c) ∈ Icc (1, 1, 1) (X, X, X)

@[simp]

theorem Finset.coe_ABCExceptionsBelow (μ : ℝ) (X : ℕ) : ↑(ABCExceptionsBelow μ X) = Set.ABCExceptionsBelow μ X

noncomputable def countTriples (μ : ℝ) (X : ℕ) : ℕ

The number of exceptions to the ABC conjecture for a given μ which are bounded by X. countTriples μ X is written as $$N_λ(X)$$ in the paper and blueprint, note that we use μ instead of λ to avoid confusion with the λ notation in Lean.

theorem countTriples_eq_finset_card (μ : ℝ) (X : ℕ) : countTriples μ X = (Finset.ABCExceptionsBelow μ X).card

def ABCExceptions (ε : ℝ) : Set (ℕ × ℕ × ℕ)

The set of exceptions to the ABC conjecture for ε, in particular the set of triples (a, b, c) which are

• pairwise coprime,
• positive,
• satisfy a + b = c,
• have radical (a * b * c) ^ (1 + ε) < c

@[simp]

theorem Set.mem_ABCExceptions (ε : ℝ) (a b c : ℕ) : (a, b, c) ∈ ABCExceptions ε ↔ 0 < a ∧ 0 < b ∧ 0 < c ∧ a.Coprime b ∧ a.Coprime c ∧ b.Coprime c ∧ a + b = c ∧ ↑(UniqueFactorizationMonoid.radical (a * b * c)) ^ (1 + ε) < ↑c

theorem ABCExceptions_subset_Ici_one (ε : ℝ) : ABCExceptions ε ⊆ Set.Ici 1

def ABCConjecture : Prop

The ABC conjecture: the set of exceptional triples is finite.

theorem ABCExceptionsBelow_eq_ABCExceptions_inter (μ : ℝ) (X : ℕ) (hμ₀ : 0 < μ) : Set.ABCExceptionsBelow μ X = ABCExceptions (μ⁻¹ - 1) ∩ Set.Icc (1, 1, 1) (X, X, X)

theorem ABCExceptionsBelow_eq_ABCExceptions_inter' (ε : ℝ) (X : ℕ) (hε : 0 < ε) : Set.ABCExceptionsBelow (1 + ε)⁻¹ X = ABCExceptions ε ∩ Set.Icc (1, 1, 1) (X, X, X)

theorem ciSup_eq_monotonicSequenceLimit {α : Type u_1} [ConditionallyCompleteLattice α] [WellFoundedGT α] (a : ℕ →o α) (ha : BddAbove (Set.range ⇑a)) : iSup ⇑a = monotonicSequenceLimit a

theorem forall_increasing' {α : Type u_1} (f : ℕ → Set α) (hf : Monotone f) (hf' : ∀ (n : ℕ), (f n).Finite) {C : ℕ} (hC : ∀ (n : ℕ), (f n).ncard ≤ C) : (⋃ (n : ℕ), f n).Finite

theorem forall_increasing {α : Type u_1} (f : ℕ → Set α) (hf : Monotone f) {s : Set α} (hf' : ∀ (n : ℕ), (s ∩ f n).Finite) {C : ℕ} (hC : ∀ (n : ℕ), (s ∩ f n).ncard ≤ C) : (s ∩ ⋃ (n : ℕ), f n).Finite

theorem GCongr.Prod.mk_le_mk {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a₁ a₂ : α) (b₁ b₂ : β) (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : (a₁, b₁) ≤ (a₂, b₂)

theorem GCongr.Prod.mk_left {α : Type u_1} {β : Type u_2} [Preorder α] [LE β] (a : α) (b₁ b₂ : β) (hb : b₁ ≤ b₂) : (a, b₁) ≤ (a, b₂)

theorem abcConjecture_iff : ABCConjecture ↔ ∀ μ > 0, μ < 1 → (fun (x : ℕ) => ↑(countTriples μ x)) =O[Filter.atTop] fun (x : ℕ) => 1

def similar (x X : ℝ) : Prop

We define reals x and X to be similar if x ∈ [X, 2X].

theorem similar_pow_natLog (x : ℕ) (hx : x ≠ 0) : similar (↑x) (2 ^ Nat.log 2 x)

noncomputable def dyadicPoints (α β γ : ℝ) (X : ℕ) : Finset (ℕ × ℕ × ℕ)

The finite set of exceptions (a, b, c) to the ABC conjecture for which X/2 ≤ c ≤ X and rad a ~ X^α, rad b ~ X^β, rad c ~ X^γ. S* counts the size of this set.

@[simp]

theorem mem_dyadicPoints (α β γ : ℝ) (X a b c : ℕ) : (a, b, c) ∈ dyadicPoints α β γ X ↔ 0 < a ∧ 0 < b ∧ 0 < c ∧ a.Coprime b ∧ a.Coprime c ∧ b.Coprime c ∧ a + b = c ∧ similar (↑(UniqueFactorizationMonoid.radical a)) (↑X ^ α) ∧ similar (↑(UniqueFactorizationMonoid.radical b)) (↑X ^ β) ∧ similar (↑(UniqueFactorizationMonoid.radical c)) (↑X ^ γ) ∧ X ≤ 2 * c ∧ c ≤ X

noncomputable def refinedCountTriplesStar (α β γ : ℝ) (X : ℕ) : ℕ

This is $$S^*_{α,β,γ}(X)$$ in the paper and blueprint.

theorem Nat.Coprime.isRelPrime (a b : ℕ) (h : a.Coprime b) : IsRelPrime a b

theorem Finset.ABCExceptionsBelow_subset_union_dyadicPoints (μ : ℝ) (X : ℕ) : ABCExceptionsBelow μ X ⊆ (indexSet✝ μ X).biUnion fun (x : ℕ × ℕ × ℕ × ℕ) => match x with | (i, j, k, n) => dyadicPoints (↑i / ↑n) (↑j / ↑n) (↑k / ↑n) (2 ^ n)

theorem sum_le_card_mul_sup {ι : Type u_1} (f : ι → ℕ) (s : Finset ι) : ∑ i ∈ s, f i ≤ s.card * s.sup f

theorem card_union_dyadicPoints_le_log_pow_mul_sup (μ : ℝ) (X : ℕ) : ((indexSet✝ μ X).biUnion fun (x : ℕ × ℕ × ℕ × ℕ) => match x with | (i, j, k, n) => dyadicPoints (↑i / ↑n) (↑j / ↑n) (↑k / ↑n) (2 ^ n)).card ≤ (Nat.log 2 X + 1) ^ 4 * (indexSet✝ μ X).sup fun (x : ℕ × ℕ × ℕ × ℕ) => match x with | (i, j, k, n) => refinedCountTriplesStar (↑i / ↑n) (↑j / ↑n) (↑k / ↑n) (2 ^ n)

noncomputable def dyadicSupBound (μ : ℝ) (X : ℕ) : ℕ

The supremum that appears in lemma 2.2, taken over a finite subset of α, β, γ > 0 such that α + β + γ ≤ μ

theorem countTriples_le_log_pow_mul_sup (μ : ℝ) (X : ℕ) : countTriples μ X ≤ (Nat.log 2 X + 1) ^ 4 * dyadicSupBound μ X

theorem Real.natLog_isBigO_logb (b : ℕ) : (fun (x : ℕ) => ↑(Nat.log b x)) =O[Filter.atTop] fun (x : ℕ) => logb ↑b ↑x

theorem Real.logb_isBigO_log (b : ℝ) : logb b =O[Filter.atTop] log

theorem Real.log_isBigO_logb (b : ℝ) (hb : 1 < b) : log =O[Filter.atTop] logb b

theorem Nat.log_isBigO_log (b : ℕ) : (fun (x : ℕ) => ↑(log b x)) =O[Filter.atTop] fun (x : ℕ) => Real.log ↑x

theorem countTriples_isBigO_dyadicSup : (fun (x : ℕ × ℝ) => match x with | (X, μ) => ↑(countTriples μ X)) =O[Filter.atTop ×ˢ ⊤] fun (x : ℕ × ℝ) => match x with | (X, μ) => Real.log ↑X ^ 4 * ↑(dyadicSupBound μ X)

def dyadicTuples {d : ℕ} (X : Fin d → ℕ) : Finset (Fin d → ℕ)

The finite set of d-tuples a i such that a i ~ X i for all i.

@[simp]

theorem mem_dyadicTuples {d : ℕ} (X x : Fin d → ℕ) : x ∈ dyadicTuples X ↔ ∀ (i : Fin d), similar ↑(x i) ↑(X i)

noncomputable def B_finset (d : ℕ) (C : Fin 3 → ℕ) (X Y Z : Fin d → ℕ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ))

The finite set counted by B_d(C, X, Y, X). We choose to add C as an entry in these tuples, as this allows us to write down a surjective map from a union of these sets back to triples (a, b, c) in dyadicTriples α β γ.

theorem mem_B_finset (d : ℕ) (C : Fin 3 → ℕ) (X Y Z x y z : Fin d → ℕ) (c : Fin 3 → ℕ) : (x, y, z, c) ∈ B_finset d C X Y Z ↔ C = c ∧ (∀ (i : Fin d), similar ↑(x i) ↑(X i)) ∧ (∀ (i : Fin d), similar ↑(y i) ↑(Y i)) ∧ (∀ (i : Fin d), similar ↑(z i) ↑(Z i)) ∧ c 0 * ∏ i : Fin d, x i ^ (↑i + 1) + c 1 * ∏ i : Fin d, y i ^ (↑i + 1) = c 2 * ∏ i : Fin d, z i ^ (↑i + 1) ∧ (c 0 * ∏ i : Fin d, x i).gcd (c 1 * ∏ i : Fin d, y i) = 1 ∧ (c 0 * ∏ i : Fin d, x i).gcd (c 2 * ∏ i : Fin d, z i) = 1 ∧ (c 1 * ∏ i : Fin d, y i).gcd (c 2 * ∏ i : Fin d, z i) = 1

noncomputable def B (d : ℕ) (c : Fin 3 → ℕ) (X Y Z : Fin d → ℕ) : ℕ

Definition 2.4

theorem Nat.factorization_le_right (p n : ℕ) (hp : Prime p) : n.factorization p ≤ n

theorem Nat.ceil_lt_floor (a b : ℝ) (ha : 0 ≤ a) (hab : a + 2 ≤ b) : ⌈a⌉₊ < ⌊b⌋₊

class NiceFactorization.ProofData : Type

The data and assumptions of lemma 2.5. We treat d as a free variable constrained by hd here because d appears in a type and this gives the user some leeway to rewrite the value of d.

• ε : ℝ

  The value of epsilon in Lemma 2.5

• hε_pos : 0 < ε
• hε : ε < 1 / 2
• d : ℕ

  d in Lemma 2.5

• hd : d = ⌊5 / 2 * ε⁻¹ ^ 2⌋₊
• n : ℕ

  n in Lemma 2.5

• X : ℕ

  X in Lemma 2.5

• h1n : 1 ≤ n
• hnX : n ≤ X

def NiceFactorization.y [data : ProofData] (j : ℕ) : ℕ

y j is the product of primes dividing n with multiplicity j.

theorem Nat.prod_squarefree {ι : Type u_1} (f : ι → ℕ) {s : Finset ι} (hf : ∀ i ∈ s, Squarefree (f i)) (h : (↑s).Pairwise (Function.onFun Coprime f)) : Squarefree (∏ i ∈ s, f i)

theorem Associated.nat_eq {a b : ℕ} (h : Associated a b) : a = b

theorem NiceFactorization.y_squarefree [data : ProofData] {i : ℕ} : Squarefree (y i)

noncomputable def NiceFactorization.K [data : ProofData] : ℕ

K in the proof of lemma 2.5

noncomputable def NiceFactorization.x [data : ProofData] (j : Fin ProofData.d) : ℕ

x in the proof of lemma 2.5

theorem NiceFactorization.x_pos [data : ProofData] (j : Fin ProofData.d) : 0 < x j

noncomputable def NiceFactorization.c [data : ProofData] : ℕ

c in the proof of lemma 2.5

theorem NiceFactorization.nat_eq_fin_iff {n a : ℕ} {b : Fin n} [NeZero n] (ha : a < n) : ↑a = b ↔ a = ↑b

theorem NiceFactorization.fin_eq_nat_iff {n a : ℕ} {b : Fin n} [NeZero n] (ha : a < n) : b = ↑a ↔ ↑b = a

theorem NiceFactorization.x_K_le_X_pow [data : ProofData] : ↑(x (↑K - 1)) ≤ ↑ProofData.X ^ ProofData.ε

theorem NiceFactorization.exists_nice_factorization [data : ProofData] : ∃ (x : Fin ProofData.d → ℕ) (c : ℕ), ProofData.n = c * ∏ j : Fin ProofData.d, x j ^ (↑j + 1) ∧ ↑c ≤ ↑ProofData.X ^ ProofData.ε ∧ (∀ (i j : Fin ProofData.d), i ≠ j → (x i).gcd (x j) = 1) ∧ ↑ProofData.X ^ (-ProofData.ε) * ↑(∏ j : Fin ProofData.d, x j) ≤ ↑(UniqueFactorizationMonoid.radical ProofData.n) ∧ ↑(UniqueFactorizationMonoid.radical ProofData.n) ≤ ↑ProofData.X ^ ProofData.ε * ↑(∏ j : Fin ProofData.d, x j)

theorem exists_nice_factorization {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) {d : ℕ} (hd : d = ⌊5 / 2 * ε⁻¹ ^ 2⌋₊) {n X : ℕ} (h1n : 1 ≤ n) (hnX : n ≤ X) : ∃ (x : Fin d → ℕ) (c : ℕ), n = c * ∏ j : Fin d, x j ^ (↑j + 1) ∧ ↑c ≤ ↑X ^ ε ∧ (∀ (i j : Fin d), i ≠ j → (x i).gcd (x j) = 1) ∧ ↑X ^ (-ε) * ↑(∏ j : Fin d, x j) ≤ ↑(UniqueFactorizationMonoid.radical n) ∧ ↑(UniqueFactorizationMonoid.radical n) ≤ ↑X ^ ε * ↑(∏ j : Fin d, x j) ∧ 0 < c ∧ (∀ (i : Fin d), 0 < x i) ∧ ∀ (i : Fin d), x i ≤ X

Proposition 2.5. The bulk of the proof is in the section NiceFactorization.

theorem exists_nice_factorization' {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) {d : ℕ} (hd : d = ⌊10 * ε⁻¹ ^ 4⌋₊) {n X : ℕ} (h1n : 1 ≤ n) (hnX : n ≤ X) (α : ℝ) (hsim : similar (↑(UniqueFactorizationMonoid.radical n)) (↑X ^ α)) : ∃ (x : Fin d → ℕ) (c : ℕ), n = c * ∏ j : Fin d, x j ^ (↑j + 1) ∧ ↑c ≤ ↑X ^ ε ^ 2 ∧ c ≤ ⌊↑X ^ (ε / 4)⌋₊ ∧ (∀ (i j : Fin d), i ≠ j → (x i).gcd (x j) = 1) ∧ ↑X ^ (α - ε) ≤ ↑(∏ j : Fin d, x j) ∧ ↑(∏ j : Fin d, x j) ≤ 2 * ↑X ^ (α + ε) ∧ 0 < c ∧ (∀ (i : Fin d), 0 < x i) ∧ ∀ (i : Fin d), x i ≤ X

Some basic consequences of Proposition 2.5, phrased in a way that make them more useful in the proof of Proposition 2.6.

def B_to_triple {d : ℕ} : (Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ) → ℕ × ℕ × ℕ

A surjective map ⋃_{c, X, Y ,Z} B (c, X, Y, Z) → S*_α β γ (X)

noncomputable def indexSet' (α β γ : ℝ) (d x : ℕ) (ε : ℝ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ))

The finite set over which we will take a supremum in proposition 2.6

theorem card_indexSet'_le (α β γ : ℝ) (d x : ℕ) (ε : ℝ) : (indexSet' α β γ d x ε).card ≤ (Nat.log 2 x + 1) ^ (3 * d) * ⌊↑x ^ (ε / 4)⌋₊ ^ 3

noncomputable def BUnion (α β γ : ℝ) {d : ℕ} (x : ℕ) (ε : ℝ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ))

The union of B-sets used in the proof of proposition 2.6.

theorem similar_pow_log {x : ℕ} (hx : 0 < x) : similar (↑x) (2 ^ Nat.log 2 x)

theorem coprime_mul_prod_aux {ι : Type u_1} {s : Finset ι} {f g u v : ι → ℕ} {a b : ℕ} (hu : ∀ (i : ι), 0 < u i) (hv : ∀ (i : ι), 0 < v i) (hcop : (a * ∏ i ∈ s, f i ^ u i).Coprime (b * ∏ i ∈ s, g i ^ v i)) : (a * ∏ i ∈ s, f i).Coprime (b * ∏ i ∈ s, g i)

theorem Nat.sum_Ico_choose (n k : ℕ) : ∑ m ∈ Finset.Ico k n, m.choose k = n.choose (k + 1)

theorem Nat.sum_range_add_choose' (n k : ℕ) : ∑ i ∈ Finset.range n, (i + k).choose k = (n + k).choose (k + 1)

theorem sum_range_id_add_one {d : ℕ} : ∑ i ∈ Finset.range d, (i + 1) = (d + 1).choose 2

theorem B_to_triple_surjOn {α β γ : ℝ} (x : ℕ) (ε : ℝ) (hε_pos : 0 < ε) (hε : ε < 1 / 2) {d : ℕ} (hd : d = ⌊10 * ε⁻¹ ^ 4⌋₊) : Set.SurjOn B_to_triple ↑(BUnion α β γ x ε) ↑(dyadicPoints α β γ x)

theorem refinedCountTriplesStar_le_card_BUnion (α β γ : ℝ) {d : ℕ} (x : ℕ) (ε : ℝ) (hε_pos : 0 < ε) (hε : ε < 1 / 2) (hd : d = ⌊10 * ε⁻¹ ^ 4⌋₊) : refinedCountTriplesStar α β γ x ≤ (BUnion α β γ x ε).card

theorem log_le_const_mul_pow {ε : ℝ} (hε : 0 < ε) (d : ℕ) (hd : 0 < d) : ∃ c ≥ 0, ∀ (x : ℕ), Real.log ↑x ^ d ≤ c * ↑x ^ ε

theorem tmp {ε : ℝ} (hε : 0 < ε) (d : ℕ) (hd : 0 < d) : ∃ (c : ℝ), ∀ (x : ℕ), 2 ≤ x → (↑(Nat.log 2 x) + 1) ^ (3 * d) ≤ c * ↑x ^ (ε / 4)

noncomputable def const (ε : ℝ) : ℝ

The implicit constant in the conclusion of proposition 2.6

theorem const_spec {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) : let d := ⌊10 * ε⁻¹ ^ 4⌋₊; ∀ (x : ℕ), 2 ≤ x → (↑(Nat.log 2 x) + 1) ^ (3 * d) ≤ const ε * ↑x ^ (ε / 4)

theorem const_nonneg {ε : ℝ} : 0 ≤ const ε

theorem card_indexSet'_le_pow (ε α β γ : ℝ) (d x : ℕ) (hd : d = ⌊10 * ε⁻¹ ^ 4⌋₊) (hx : 2 ≤ x) (hε_pos : 0 < ε) (hε : ε < 1 / 2) : ↑(indexSet' α β γ d x ε).card ≤ const ε * ↑x ^ ε

noncomputable def d (ε : ℝ) : ℕ

The value of d chosen in proposition 2.6

theorem refinedCountTriplesStar_isBigO_B {α β γ : ℝ} {x : ℕ} (h2X : 2 ≤ x) {ε : ℝ} (hε_pos : 0 < ε) (hε : ε < 1 / 2) : ∃ (s : Finset ((Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin 3 → ℕ))), ↑(refinedCountTriplesStar α β γ x) ≤ const ε * ↑x ^ ε * ↑(s.sup fun (x : (Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin (d ε) → ℕ) × (Fin 3 → ℕ)) => match x with | (X, Y, Z, c) => B (d ε) c X Y Z) ∧ ∀ (X Y Z : Fin (d ε) → ℕ) (c : Fin 3 → ℕ), (X, Y, Z, c) ∈ s → ↑x ^ (α - ε) ≤ 2 ^ d ε * ↑(∏ j : Fin (d ε), X j) ∧ ↑(∏ j : Fin (d ε), X j) ≤ 2 * ↑x ^ (α + ε) ∧ ↑x ^ (β - ε) ≤ 2 ^ d ε * ↑(∏ j : Fin (d ε), Y j) ∧ ↑(∏ j : Fin (d ε), Y j) ≤ 2 * ↑x ^ (β + ε) ∧ ↑x ^ (γ - ε) ≤ 2 ^ d ε * ↑(∏ j : Fin (d ε), Z j) ∧ ↑(∏ j : Fin (d ε), Z j) ≤ 2 * ↑x ^ (γ + ε) ∧ ∏ i : Fin (d ε), X i ^ (↑i + 1) ≤ x ∧ ∏ i : Fin (d ε), Y i ^ (↑i + 1) ≤ x ∧ ∏ i : Fin (d ε), Z i ^ (↑i + 1) ≤ x ∧ ↑x ^ (1 - ε ^ 2) ≤ 2 ^ ((d ε + 1).choose 2 + 1) * ↑(∏ i : Fin (d ε), Z i ^ (↑i + 1)) ∧ (c 0).Coprime (c 1) ∧ (c 1).Coprime (c 2) ∧ (c 0).Coprime (c 2) ∧ (∀ (i : Fin 3), 1 ≤ c i) ∧ ∀ (i : Fin 3), ↑(c i) ≤ ↑x ^ ε