Google DeepMind; Formal Conjectures authors

ABC.abc

ABC.abc

∀ (ε : ℝ), 0 < ε → {(a, b, c) | 0 < a ∧ 0 < b ∧ 0 < c ∧ {a, b, c}.Pairwise Nat.Coprime ∧ a + b = c ∧ ↑(ABC.radical (a * b * c)) ^ (1 + ε) < ↑c}.Finite

ABC.abc.variants.lt_constant_mul

ABC.abc.variants.lt_constant_mul

∀ (ε : ℝ), 0 < ε → ∃ K, ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → {a, b, c}.Pairwise Nat.Coprime → a + b = c → ↑c < K * ↑(ABC.radical (a * b * c)) ^ (1 + ε)

ABC.abc.variants.quality

ABC.abc.variants.quality

∀ (ε : ℝ), 0 < ε → {(a, b, c) | 0 < a ∧ 0 < b ∧ 0 < c ∧ {a, b, c}.Pairwise Nat.Coprime ∧ a + b = c ∧ ABC.quality a b c > 1 + ε}.Finite

ABC.radical_12

ABC.radical_12

ABC.radical 12 = 6

ABC.radical_16

ABC.radical_16

ABC.radical 16 = 2

ABC.radical_17

ABC.radical_17

ABC.radical 17 = 17

AgohGiuga.agoh_giuga

AgohGiuga.agoh_giuga

AgohGiuga.AgohGiugaCongr

AgohGiuga.agoh_giuga.variants.equivalence

AgohGiuga.agoh_giuga.variants.equivalence

AgohGiuga.AgohGiugaCongr ↔ AgohGiuga.AgohGiugaSum

AgohGiuga.agoh_giuga.variants.giuga

AgohGiuga.agoh_giuga.variants.giuga

AgohGiuga.AgohGiugaSum

AgohGiuga.agoh_giuga.variants.isStrongGiuga_growth

AgohGiuga.agoh_giuga.variants.isStrongGiuga_growth

∀ (G : ℕ → ℕ), (G = fun x => (Finset.filter AgohGiuga.IsStrongGiuga (Finset.Icc 1 x)).card) → ∃ N O, ∀ n ≥ N, ↑(G n) ≤ O * √↑n * Real.log ↑n

AgohGiuga.agoh_giuga.variants.isStrongGiuga_implies_isCarmichael

AgohGiuga.agoh_giuga.variants.isStrongGiuga_implies_isCarmichael

∀ (a : ℕ), AgohGiuga.IsStrongGiuga a → IsCarmichael a

AgohGiuga.agoh_giuga.variants.le_primeFactors_card_of_isStrongGiuga

AgohGiuga.agoh_giuga.variants.le_primeFactors_card_of_isStrongGiuga

∀ (a : ℕ), AgohGiuga.IsStrongGiuga a → 9 ≤ a.primeFactors.card

AgohGiuga.isCarmichael_561

AgohGiuga.isCarmichael_561

IsCarmichael 561

AgohGiuga.isStrongGiuga_iff

AgohGiuga.isStrongGiuga_iff

∀ {a : ℕ}, a.Composite → (AgohGiuga.IsStrongGiuga a ↔ IsCarmichael a ∧ ∃ n, ∑ p ∈ a.primeFactors, 1 / ↑p - 1 / ↑a = ↑n)

AgohGiuga.isWeakGiuga_iff_prime_dvd

AgohGiuga.isWeakGiuga_iff_prime_dvd

∀ {n : ℕ}, n.Composite → (AgohGiuga.IsWeakGiuga n ↔ ∀ p ∈ n.primeFactors, p ∣ n / p - 1)

AgohGiuga.isWeakGiuga_iff_sum_primeFactors

AgohGiuga.isWeakGiuga_iff_sum_primeFactors

∀ {n : ℕ}, n.Composite → (AgohGiuga.IsWeakGiuga n ↔ ∃ m, ∑ p ∈ n.primeFactors, 1 / ↑p - 1 / ↑n = ↑m)

AgohGiuga.korselts_criterion

AgohGiuga.korselts_criterion

∀ (a : ℕ), a.Composite → (IsCarmichael a ↔ Squarefree a ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ a → p - 1 ∣ a - 1)

AgohGiuga.squarefree_of_isCarmichael

AgohGiuga.squarefree_of_isCarmichael

∀ {a : ℕ}, a.Composite → IsCarmichael a → Squarefree a

AgrawalConjecture.agrawal_conjecture

AgrawalConjecture.agrawal_conjecture

True ↔ ∀ (n r : ℕ), n > 1 → r > 0 → n.gcd r = 1 → let R := Polynomial (ZMod n); have X := Polynomial.X; have I := Ideal.span {X ^ r - 1}; (Ideal.Quotient.mk I) ((X - 1) ^ n) = (Ideal.Quotient.mk I) (X ^ n - 1) → Nat.Prime n ∨ ↑n ^ 2 = 1

AgrawalConjecture.agrawal_conjecture.variants.popovych

AgrawalConjecture.agrawal_conjecture.variants.popovych

∀ (n r : ℕ), n > 1 → r > 0 → n.gcd r = 1 → let R := Polynomial (ZMod n); have X := Polynomial.X; have I := Ideal.span {X ^ r - 1}; (Ideal.Quotient.mk I) ((X - 1) ^ n) = (Ideal.Quotient.mk I) (X ^ n - 1) → (Ideal.Quotient.mk I) ((X + 2) ^ n) = (Ideal.Quotient.mk I) (X ^ n + 2) → Nat.Prime n ∨ ↑n ^ 2 = 1