Borwein-Style Lower Bound

Any counterexample to the Agoh-Giuga conjecture exceeds 10^13800.

The proof combines three ingredients:

1. Branch-and-bound verifier: every normal odd-prime set with reciprocal sum > 1 has at least B elements (computational search via native_decide).

2. Structural transfer: a Carmichael-Giuga number's prime factors form such a set, so B ≤ n.primeFactors.card, hence ∏_{j<B} (j+1)-th prime ≤ n.

3. Product comparison: the product of the first 4000 odd primes exceeds 10^13800.

The full pipeline is demonstrated at B = 20 (~2s). The main theorem's sorry reduces to running the verifier at B = 4000.

Section 1 — Borwein definitions

def Borwein.IsOddPrimeSet (S : Finset ℕ) : Prop

A finite set whose elements are odd primes.

Equations

• Borwein.IsOddPrimeSet S = ∀ p ∈ S, Nat.Prime p ∧ Odd p

def Borwein.reciprocalSum (S : Finset ℕ) : ℚ

Reciprocal sum used in the Giuga/Borwein inequalities.

Equations

• Borwein.reciprocalSum S = ∑ p ∈ S, 1 / ↑p

def Borwein.IsNormalSet (S : Finset ℕ) : Prop

A set of primes is normal if no distinct pair has one prime dividing the other minus one.

Equations

• Borwein.IsNormalSet S = ∀ ⦃p q : ℕ⦄, p ∈ S → q ∈ S → p ≠ q → ¬p ∣ q - 1

Section 2 — Structural bridge

theorem IsCarmichaelNumber.primeFactors_isNormal {n : ℕ} (hc : IsCarmichaelNumber n) : Borwein.IsNormalSet n.primeFactors

For Carmichael numbers, the set of prime factors is normal in the Borwein sense: no distinct prime factor divides another minus one.

theorem IsGiugaNumber.one_lt_reciprocalSum_primeFactors {n : ℕ} (hg : IsGiugaNumber n) : 1 < Borwein.reciprocalSum n.primeFactors

Repackaging the existing reciprocal-sum theorem with the Borwein notation.

theorem carmichael_giuga_product_le_of_card_bound {n k : ℕ} (hc : IsCarmichaelNumber n) (_hg : IsGiugaNumber n) (hcard : k ≤ n.primeFactors.card) : ∏ j ∈ Finset.range k, Nat.nth Nat.Prime (j + 1) ≤ n

If a Carmichael-Giuga number has at least k prime factors, then it is at least the product of the first k odd primes.

Section 3 — Branch-and-bound verifier

Unnormalized positive fractions

structure BorweinVerifier.UFrac : Type

Unnormalized positive fraction: represents num / den. No GCD normalization — arithmetic is fast at the cost of growing numerators and denominators. Only used for comparisons (via cross-multiplication).

• num : ℕ
• den : ℕ

instance BorweinVerifier.instDecidableEqUFrac : DecidableEq UFrac

Equations

• BorweinVerifier.instDecidableEqUFrac = BorweinVerifier.instDecidableEqUFrac.decEq

def BorweinVerifier.instDecidableEqUFrac.decEq (x✝ x✝¹ : UFrac) : Decidable (x✝ = x✝¹)

Equations

• BorweinVerifier.instDecidableEqUFrac.decEq { num := a, den := a_1 } { num := b, den := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance BorweinVerifier.instInhabitedUFrac : Inhabited UFrac

Equations

• BorweinVerifier.instInhabitedUFrac = { default := { num := 0, den := 1 } }

def BorweinVerifier.UFrac.zero : UFrac

Zero as a fraction.

Equations

• BorweinVerifier.UFrac.zero = { num := 0, den := 1 }

def BorweinVerifier.UFrac.addRecip (f : UFrac) (p : ℕ) : UFrac

Add the reciprocal of p to the fraction: a/b + 1/p = (a*p + b)/(b*p).

Equations

• f.addRecip p = { num := f.num * p + f.den, den := f.den * p }

def BorweinVerifier.UFrac.sumLtOne (f g : UFrac) : Bool

Check if a/b + c/d < 1, i.e., a*d + c*b < b*d.

Equations

• f.sumLtOne g = decide (f.num * g.den + g.num * f.den < f.den * g.den)

def BorweinVerifier.UFrac.leOne (f : UFrac) : Bool

Check if a/b ≤ 1, i.e., a ≤ b.

Equations

• f.leOne = decide (f.num ≤ f.den)

UFrac interpretation in ℚ

noncomputable def BorweinVerifier.UFrac.toRat (f : UFrac) : ℚ

Interpret a UFrac as a rational number.

Equations

• f.toRat = ↑f.num / ↑f.den

theorem BorweinVerifier.UFrac.zero_toRat : zero.toRat = 0

theorem BorweinVerifier.UFrac.zero_den_pos : 0 < zero.den

theorem BorweinVerifier.UFrac.addRecip_den_pos (f : UFrac) (p : ℕ) (hf : 0 < f.den) (hp : 0 < p) : 0 < (f.addRecip p).den

theorem BorweinVerifier.UFrac.addRecip_sound (f : UFrac) (p : ℕ) (hf : 0 < f.den) (hp : 0 < p) : (f.addRecip p).toRat = f.toRat + 1 / ↑p

theorem BorweinVerifier.UFrac.sumLtOne_sound (f g : UFrac) (hf : 0 < f.den) (hg : 0 < g.den) (h : f.sumLtOne g = true) : f.toRat + g.toRat < 1

theorem BorweinVerifier.UFrac.leOne_sound (f : UFrac) (hd : 0 < f.den) (h : f.leOne = true) : f.toRat ≤ 1

Prime enumeration utilities

def BorweinVerifier.isPrime (n : ℕ) : Bool

Check primality by trial division.

Equations

• BorweinVerifier.isPrime n = if n < 2 then false else BorweinVerifier.isPrime.go n 2 n

def BorweinVerifier.isPrime.go (n d : ℕ) : ℕ → Bool

Equations

• BorweinVerifier.isPrime.go n d 0 = true
• BorweinVerifier.isPrime.go n d fuel.succ = if d * d > n then true else if n % d = 0 then false else BorweinVerifier.isPrime.go n (d + 1) fuel

theorem BorweinVerifier.isPrime_sound {n : ℕ} (h : isPrime n = true) : Nat.Prime n

isPrime n = true → Nat.Prime n

theorem BorweinVerifier.isPrime_complete {n : ℕ} (h : Nat.Prime n) : isPrime n = true

Nat.Prime n → isPrime n = true

def BorweinVerifier.nextOddPrime (start fuel : ℕ) : Option ℕ

Find the next odd prime ≥ start, within fuel candidates.

Equations

• BorweinVerifier.nextOddPrime start fuel = BorweinVerifier.nextOddPrime.go (if start ≤ 3 then 3 else if start % 2 = 0 then start + 1 else start) fuel

def BorweinVerifier.nextOddPrime.go : ℕ → ℕ → Option ℕ

Equations

• BorweinVerifier.nextOddPrime.go x✝ 0 = none
• BorweinVerifier.nextOddPrime.go x✝ fuel.succ = if BorweinVerifier.isPrime x✝ = true then some x✝ else BorweinVerifier.nextOddPrime.go (x✝ + 2) fuel

theorem BorweinVerifier.nextOddPrime_sound {start fuel p : ℕ} (h : nextOddPrime start fuel = some p) : Nat.Prime p ∧ Odd p ∧ start ≤ p

Top-level soundness for nextOddPrime: if it returns some p, then p is prime, odd, and p ≥ start.

def BorweinVerifier.isAdmissible (current : Array ℕ) (p : ℕ) : Bool

Check two-way normality: p is admissible to add to the set current.

Equations

• BorweinVerifier.isAdmissible current p = current.all fun (q : ℕ) => !decide (q ∣ p - 1) && !decide (p ∣ q - 1)

theorem BorweinVerifier.isAdmissible_sound {current : Array ℕ} {p : ℕ} (h : isAdmissible current p = true) (q : ℕ) : q ∈ current.toList → ¬q ∣ p - 1 ∧ ¬p ∣ q - 1

isAdmissible current p = true means p is two-way normal w.r.t. every element of current.

def BorweinVerifier.nextAdmissible (current : Array ℕ) (start probeFuel : ℕ) : Option ℕ

Find the next admissible odd prime ≥ start w.r.t. current.

Equations

• BorweinVerifier.nextAdmissible current start probeFuel = BorweinVerifier.nextAdmissible.go current start probeFuel

def BorweinVerifier.nextAdmissible.go (current : Array ℕ) : ℕ → ℕ → Option ℕ

Equations

• One or more equations did not get rendered due to their size.
• BorweinVerifier.nextAdmissible.go current x✝ 0 = none

theorem BorweinVerifier.nextAdmissible_sound {current : Array ℕ} {start probeFuel p : ℕ} (h : nextAdmissible current start probeFuel = some p) : Nat.Prime p ∧ Odd p ∧ start ≤ p ∧ ∀ q ∈ current.toList, ¬q ∣ p - 1 ∧ ¬p ∣ q - 1

If nextAdmissible returns some p, then p is prime, odd, p ≥ start, and admissible w.r.t. current.

Tail bound

def BorweinVerifier.tailBound (start count probeFuel : ℕ) : UFrac

Upper bound on the reciprocal sum achievable by adding at most count primes ≥ start. We sum reciprocals of the next count primes ≥ start (ignoring normality, which makes this a valid over-estimate).

Equations

• BorweinVerifier.tailBound start count probeFuel = BorweinVerifier.tailBound.go start count probeFuel BorweinVerifier.UFrac.zero

def BorweinVerifier.tailBound.go : ℕ → ℕ → ℕ → UFrac → UFrac

Equations

• One or more equations did not get rendered due to their size.
• BorweinVerifier.tailBound.go x✝² 0 x✝¹ x✝ = x✝
• BorweinVerifier.tailBound.go x✝² x✝¹ 0 x✝ = x✝

def BorweinVerifier.tailBoundFound (start count probeFuel : ℕ) : ℕ

Count of primes found by tailBound. Returns the number of primes actually summed (may be less than count if fuel runs out).

Equations

• BorweinVerifier.tailBoundFound start count probeFuel = BorweinVerifier.tailBoundFound.go start count probeFuel 0

def BorweinVerifier.tailBoundFound.go : ℕ → ℕ → ℕ → ℕ → ℕ

Equations

• One or more equations did not get rendered due to their size.
• BorweinVerifier.tailBoundFound.go x✝² 0 x✝¹ x✝ = x✝
• BorweinVerifier.tailBoundFound.go x✝² x✝¹ 0 x✝ = x✝

theorem BorweinVerifier.tailBound_den_pos {start count probeFuel : ℕ} : 0 < (tailBound start count probeFuel).den

Branch-and-bound verifier

def BorweinVerifier.verify (current : Array ℕ) (curSum : UFrac) (target start probeFuel : ℕ) : ℕ → Bool

Branch-and-bound verifier.

Returns true if every normal odd-prime set extending current with all additional elements ≥ start, having reciprocal sum > 1, has at least target elements.

Equations

• One or more equations did not get rendered due to their size.
• BorweinVerifier.verify current curSum target start probeFuel 0 = false

def BorweinVerifier.verifyMinNormalSet (target probeFuel depth : ℕ) : Bool

Top-level verifier: checks that every normal odd-prime set with reciprocal sum > 1 has at least target elements.

Equations

• BorweinVerifier.verifyMinNormalSet target probeFuel depth = BorweinVerifier.verify #[] BorweinVerifier.UFrac.zero target 3 probeFuel depth

Fuel check

def BorweinVerifier.fuelOK (current : Array ℕ) (curSum : UFrac) (target start probeFuel : ℕ) : ℕ → Bool

Decidable check that verify's fuel was sufficient at every node. At pruning nodes, checks tailBoundFound = remaining. At terminal nodes (nextAdmissible = none), returns false (conservative).

Equations

• One or more equations did not get rendered due to their size.
• BorweinVerifier.fuelOK current curSum target start probeFuel 0 = true

def BorweinVerifier.fuelOKTop (target probeFuel depth : ℕ) : Bool

Top-level fuel check.

Equations

• BorweinVerifier.fuelOKTop target probeFuel depth = BorweinVerifier.fuelOK #[] BorweinVerifier.UFrac.zero target 3 probeFuel depth

Soundness

structure BorweinVerifier.IsReachable (current : Array ℕ) (start : ℕ) (T : Finset ℕ) : Prop

A set T is reachable from (current, start) if it contains all elements of current, every element is an odd prime, the set is normal, and all elements not in current are ≥ start.

• oddPrime : Borwein.IsOddPrimeSet T
• normal : Borwein.IsNormalSet T
• contains (p : ℕ) : p ∈ current.toList → p ∈ T
• beyond (p : ℕ) : p ∈ T → p ∈ current.toList ∨ start ≤ p

theorem BorweinVerifier.verifyMinNormalSet_sound (target probeFuel depth : ℕ) (hVerify : verifyMinNormalSet target probeFuel depth = true) (hFuel : fuelOKTop target probeFuel depth = true) (T : Finset ℕ) : Borwein.IsOddPrimeSet T → Borwein.IsNormalSet T → 1 < Borwein.reciprocalSum T → target ≤ T.card

Top-level soundness: if verifyMinNormalSet succeeds and fuel is sufficient, then every normal odd-prime set with reciprocal sum > 1 has ≥ target elements.

Verified computations

theorem BorweinVerifier.verify_target_20 : verifyMinNormalSet 20 10000 2000 = true

The verifier confirms: every normal odd-prime set with reciprocal sum > 1 has at least 20 elements. Verified by native_decide in ~2 seconds.

theorem BorweinVerifier.fuelOK_20 : fuelOKTop 20 10000 2000 = true

Fuel check passes for target 20.

theorem BorweinVerifier.normalSet_card_ge_20 (T : Finset ℕ) : Borwein.IsOddPrimeSet T → Borwein.IsNormalSet T → 1 < Borwein.reciprocalSum T → 20 ≤ T.card

Corollary: any normal odd-prime set with reciprocal sum > 1 has ≥ 20 elements.

Section 4 — Product comparison

theorem Nat.count_prime_le_succ (k : ℕ) : count Prime (2 * k + 3) ≤ k + 1

The number of primes less than 2k+3 is at most k+1.

theorem nth_prime_ge_two_mul_add_three (k : ℕ) : 2 * k + 3 ≤ Nat.nth Nat.Prime (k + 1)

The (k+1)-th prime (0-indexed) is at least 2k+3.

def oddNumProduct : ℕ → ℕ

Product of the first B odd numbers starting from 3: oddNumProduct B = 3 × 5 × 7 × ⋯ × (2B+1).

Equations

• oddNumProduct 0 = 1
• oddNumProduct fuel.succ = oddNumProduct fuel * (2 * fuel + 3)

theorem oddNumProduct_eq_prod_range (B : ℕ) : oddNumProduct B = ∏ j ∈ Finset.range B, (2 * j + 3)

theorem prod_odd_le_prod_nth_prime (B : ℕ) : ∏ j ∈ Finset.range B, (2 * j + 3) ≤ ∏ j ∈ Finset.range B, Nat.nth Nat.Prime (j + 1)

theorem oddNumProduct_4000_gt : 10 ^ 13800 < oddNumProduct 4000

The product of the first 4000 odd numbers ≥ 3 exceeds 10^13800.

theorem borwein_product_comparison : 10 ^ 13800 < ∏ j ∈ Finset.range 4000, Nat.nth Nat.Prime (j + 1)

The product of the first 4000 odd primes exceeds 10^13800.

Section 5 — Main theorem

def borweinBound : ℕ

The Borwein et al. (1996) lower bound: any counterexample to Agoh-Giuga exceeds 10 ^ 13800.

Equations

• borweinBound = 10 ^ 13800

theorem carmichael_giuga_card_of_verifier {n B : ℕ} (hc : IsCarmichaelNumber n) (hg : IsGiugaNumber n) (hMin : ∀ (T : Finset ℕ), Borwein.IsOddPrimeSet T → Borwein.IsNormalSet T → 1 < Borwein.reciprocalSum T → B ≤ T.card) : B ≤ n.primeFactors.card

Transfer from verifier to cardinality bound.

theorem carmichael_giuga_product_of_verifier {n B : ℕ} (hc : IsCarmichaelNumber n) (hg : IsGiugaNumber n) (hMin : ∀ (T : Finset ℕ), Borwein.IsOddPrimeSet T → Borwein.IsNormalSet T → 1 < Borwein.reciprocalSum T → B ≤ T.card) : ∏ j ∈ Finset.range B, Nat.nth Nat.Prime (j + 1) ≤ n

Transfer from verifier to product bound.

theorem carmichael_giuga_card_ge_20 {n : ℕ} (hc : IsCarmichaelNumber n) (hg : IsGiugaNumber n) : 20 ≤ n.primeFactors.card

Pipeline demo: any Carmichael-Giuga number has ≥ 20 prime factors.

theorem carmichael_giuga_borwein_bound {n : ℕ} (hc : IsCarmichaelNumber n) (hg : IsGiugaNumber n) : borweinBound < n

Main theorem: any counterexample to Agoh-Giuga exceeds 10^13800.

The remaining sorry is purely computational: running the verifier at target 4000 via native_decide. The pipeline is demonstrated at target 20.