abc conjecture to Borsuk's conjecture

Theoremabc conjecture #

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/ABC.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 3 open. It also has 3 test statements, counted here but not shown.

`ABC.abc`

Open: stated without proof.

For every positive real number ε, there exist only finitely many triples (a, b, c) of coprime positive integers, with a + b = c, such that c > rad(abc)^(1+ε)

theorem abc (ε : ℝ) (hε : 0 < ε) :
    {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ ({a, b, c} : Set ℕ).Pairwise Nat.Coprime ∧
    a + b = c ∧ (radical <| a * b * c : ℝ)^(1 + ε) < c}.Finite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ABC.lean, line 63.

`ABC.abc.variants.lt_constant_mul`

Open: stated without proof.

For every positive real number ε, there exists a constant K_ε such that for all triples (a, b, c) of coprime positive integers, with a + b = c we have c < K_ε rad(abc)^(1+ε).

theorem abc.variants.lt_constant_mul (ε : ℝ) (hε : 0 < ε) : ∃ K,
    ∀ (a b c : ℕ), 0 < a → 0 < b → 0 < c → ({a, b, c} : Set ℕ).Pairwise Nat.Coprime → a + b = c →
    c < K * (radical <| a * b * c : ℝ)^(1 + ε)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ABC.lean, line 72.

`ABC.abc.variants.quality`

Open: stated without proof.

For every positive real number ε, there exist only finitely many triples (a, b, c) of coprime positive integers with a + b = c such that q(a, b, c) > 1 + ε.

theorem abc.variants.quality (ε : ℝ) (hε : 0 < ε) :
    {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ ({a, b, c} : Set ℕ).Pairwise Nat.Coprime ∧
    a + b = c ∧ quality a b c > (1 + ε)}.Finite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ABC.lean, line 81.

Sources

LeanABC.abc · ABC.abc.variants.lt_constant_mul · ABC.abc.variants.quality

TheoremAgoh-Giuga conjecture #

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/AgohGiuga.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 14 research or textbook statements: 2 open, 10 solved and 2 textbook results. It also has 1 test statement, counted here but not shown.

`AgohGiuga.agoh_giuga`

Open: stated without proof.

The Agoh-Giuga Conjecture, Agoh's formulation

theorem agoh_giuga : AgohGiugaCongr

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 65.

`AgohGiuga.agoh_giuga.variants.giuga`

Open: stated without proof.

The Agoh-Giuga Conjecture, Giuga's formulation

theorem agoh_giuga.variants.giuga : AgohGiugaSum

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 70.

`AgohGiuga.agoh_giuga.variants.equivalence`

Solved: stated here without proof.

The two statements of the conjecture are equivalent.

theorem agoh_giuga.variants.equivalence : AgohGiugaCongr ↔ AgohGiugaSum

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 75.

`AgohGiuga.isWeakGiuga_iff_prime_dvd`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/2663234a28260853790aa5752d8d4550ff0ab1ca/FormalConjectures/Wikipedia/AgohGiuga.lean#L97.

A composite number \(n\) is weak Giuga if and only if \(p \mid (\frac{n}{p} - 1)\) for all prime divisors \(p\) of \(n\).

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

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 102.

`AgohGiuga.isWeakGiuga_iff_sum_primeFactors`

Solved: stated here without proof.

A composite number \(n\) is weak Giuga if and only if

\[ \sum_{p\mid n} \frac{1}{p} - \frac{1}{n} \in\mathbb{N}. \]

theorem isWeakGiuga_iff_sum_primeFactors {n : ℕ} (hn : n.Composite) :
    IsWeakGiuga n ↔ ∃ m : ℕ, ∑ p ∈ n.primeFactors, (1 / p : ℚ) - 1 / n = m

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 113.

`AgohGiuga.squarefree_of_isCarmichael`

Textbook result, proved here.

A composite Carmichael number is squarefree.

theorem squarefree_of_isCarmichael {a : ℕ} (ha₁ : a.Composite) (ha₂ : IsCarmichael a) :
    Squarefree a

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 119.

`AgohGiuga.korselts_criterion`

Textbook result, proved here.

A composite number a is Carmichael if and only if it is squarefree and, for all prime p dividing a, we have p - 1 ∣ a - 1.

theorem korselts_criterion (a : ℕ) (ha₁ : a.Composite) :
    IsCarmichael a ↔ Squarefree a ∧
      ∀ p, p.Prime → p ∣ a → (p - 1 : ℕ) ∣ (a - 1 : ℕ)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 135.

`AgohGiuga.isStrongGiuga_iff`

Solved: stated here without proof.

Giuga showed that a number n is strong Giuga if and only if it is Carmichael and ∑_{p|n} 1/p - 1/n ∈ ℕ (i.e., if and only if it is Carmichael and weak Giuga). Ref: G. Giuga, Su una presumibile proprieta caratteristica dei numeri primi

theorem isStrongGiuga_iff {a : ℕ} (ha : a.Composite) :
    IsStrongGiuga a ↔ IsCarmichael a ∧ ∃ n : ℕ, ∑ p ∈ a.primeFactors, (1 / p : ℚ) - 1 / a = n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 207.

`AgohGiuga.agoh_giuga.variants.isStrongGiuga_implies_isCarmichael`

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/394ec1c1ff92bdf2fa10f30d62ae9d0455d3ce20/Proofs/T_AgohGiuga_agoh_giuga_variants_isStrongGiuga_implies_isCarmichael.lean#L283.

Every strong Giuga number is a Carmichael number.

theorem agoh_giuga.variants.isStrongGiuga_implies_isCarmichael
    (a : ℕ) (ha : IsStrongGiuga a) : IsCarmichael a

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 216.

`AgohGiuga.agoh_giuga.variants.le_primeFactors_card_of_isStrongGiuga`

Solved: stated here without proof.

Giuga showed that a Giuga number has at least 9 prime factors. Ref: G. Giuga, Su una presumibile proprieta caratteristica dei numeri primi

theorem agoh_giuga.variants.le_primeFactors_card_of_isStrongGiuga
    (a : ℕ) (ha : IsStrongGiuga a) : 9 ≤ a.primeFactors.card

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 225.

`AgohGiuga.agoh_giuga.variants._1000_le_digits_length_of_isStrongGiuga`

Solved: stated here without proof.

Giuga showed that a counterexample Giuga number has at least 1000 digits. Ref: G. Giuga, Su una presumibile proprieta caratteristica dei numeri primi

theorem agoh_giuga.variants._1000_le_digits_length_of_isStrongGiuga
    (a : ℕ) (ha : IsStrongGiuga a) : 1000 ≤ (Nat.digits 10 a).length

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 234.

`AgohGiuga.agoh_giuga.variants._1700_le_digits_length_of_isStrongGiuga`

Solved: stated here without proof.

Bedocchi showed that any Giuga number has at least 1700 digits. Ref: E. Bedocchi, Note on a conjecture about prime numbers

theorem agoh_giuga.variants._1700_le_digits_length_of_isStrongGiuga
    (a : ℕ) (ha : IsStrongGiuga a) :
    (Nat.digits 10 a).length > 1700

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 243.

`AgohGiuga.agoh_giuga.variants._13000_le_digits_length_of_isStrongGiuga`

Solved: stated here without proof.

Borwein, Borwein, Borwein and Girgensohn showed that any strong Giuga number has at least 13000 digits. Ref: D. Borwein, J. M. Borwein, P. B. Borwein, and R. Girgensohn, Giuga’s conjecture on primality

theorem agoh_giuga.variants._13000_le_digits_length_of_isStrongGiuga
    (a : ℕ) (ha : IsStrongGiuga a) : 13000 ≤ (Nat.digits 10 a).length

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 254.

`AgohGiuga.agoh_giuga.variants.isStrongGiuga_growth`

Solved: stated here without proof.

Let G(X) denote the number of exceptions n ≤ X to Giuga’s conjecture. Then for X larger than an absolute constant which can be made explicit, G(X) ≪ X^{1/2} log X. Ref: Vicentiu Tipu, A Note on Giuga’s Conjecture

theorem agoh_giuga.variants.isStrongGiuga_growth
    (G : ℕ → ℕ) (hG : G = fun x => Finset.Icc 1 x |>.filter IsStrongGiuga |>.card) :
    ∃ N O, ∀ n ≥ N, G n ≤ O * (n : ℝ).sqrt * (n : ℝ).log

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AgohGiuga.lean, line 266.

Sources

TheoremAgrawal's conjecture #

Agrawal's conjecture is a stronger version of the theorem that forms the basis of the AKS primality test. If true, it would significantly improve the efficiency of primality testing.

The conjecture states that for coprime \(n\) and \(r\), if the polynomial congruence \((X-1)^n \equiv X^n-1 \pmod{n, X^r-1}\) holds, then \(n\) is either prime or \(n^2 \equiv 1 \pmod{r}\).

References: - Wikipedia - AIM Math - Paper

Quoted from FormalConjectures/Wikipedia/Agrawal.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 2 open.

`AgrawalConjecture.agrawal_conjecture`

Open: stated without proof.

Agrawal's Primality Conjecture.

Does the congruence \((X-1)^n \equiv X^n - 1 \pmod{n, X^r-1}\) imply \(n\) is prime (with a specific exception for \(n^2 \equiv 1 \pmod{r}\))?

While the "if" direction is a known theorem, the "only if" direction remains a conjecture.

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

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Agrawal.lean, line 52.

`AgrawalConjecture.agrawal_conjecture.variants.popovych`

Open: stated without proof.

Roman B. Popovych Conjecture. A stronger version of Agrawal's conjecture, which also considers the congruence \((X+2)^n \equiv X^n + 2 \pmod{n, X^r-1}\). If both congruences hold, then \(n\) is either prime or \(n^2 \equiv 1 \pmod{r}\). This variant was proposed by Roman B. Popovych in 2018.

theorem agrawal_conjecture.variants.popovych :
  ∀ (n r : ℕ), n > 1 → r > 0 → n.gcd r = 1 →
    let R := Polynomial (ZMod n)
    let X : R := Polynomial.X
    let I : Ideal R := Ideal.span ({X^r - 1} : Set R)
    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) →
    (n.Prime ∨ (n^2 : ZMod r) = 1)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Agrawal.lean, line 69.

Sources

LeanAgrawalConjecture.agrawal_conjecture · AgrawalConjecture.agrawal_conjecture.variants.popovych

TheoremNormality of Irrational Algebraic Numbers #

It is unknown whether every irrational algebraic real number is normal in any integer base. Here a real number is normal in base \(b\) if, for every \(k \ge 1\), every string of \(k\) digits appears in its base-\(b\) expansion with asymptotic frequency \(1/b^k\). The stronger conjecture that every irrational algebraic real number is absolutely normal is stated separately: normality in one base and normality in every base are not equivalent definitions.

In a 1950 note on the decimal digits of \(\sqrt{2}\), Borel [Bor50] conjectured that every irrational algebraic number is normal in every base. This was the first publication to address the expansion of an irrational algebraic number [AB07].

For the characterisation of normality by uniform distribution modulo \(1\), see FormalConjectures/Books/BugeaudDistributionModuloOne/NormalAndRich.lean.

References: - Wikipedia: Normal number - [Bor50] Borel, Émile. "Sur les chiffres décimaux de \(\sqrt{2}\) et divers problèmes de probabilités en chaîne." C. R. Acad. Sci. Paris 230 (1950): 591-593. - [AB07] Adamczewski, Boris, and Yann Bugeaud. "On the complexity of algebraic numbers I. Expansions in integer bases." Annals of Mathematics 165.2 (2007): 547-565. - [BC01] Bailey, David H., and Richard E. Crandall. "On the random character of fundamental constant expansions." Experimental Mathematics 10.2 (2001): 175-190. https://projecteuclid.org/journals/experimental-mathematics/volume-10/issue-2/On-the-random-character-of-fundamental-constant-expansions/em/999188630.full

Quoted from FormalConjectures/Wikipedia/AlgebraicNormality.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 2 open. It also has 1 API statement, counted here but not shown.

`AlgebraicNormality.irrational_algebraic_absolutely_normal`

Open: stated without proof.

Borel's normality conjecture [Bor50]: every irrational algebraic real is absolutely normal.

theorem irrational_algebraic_absolutely_normal :
    ∀ x : ℝ, IsIrrationalAlgebraic x → IsAbsolutelyNormal x

Category research open; AMS 11 Number theory, 12 Field theory and polynomials, 41 Approximations and expansions. Declared in FormalConjectures/Wikipedia/AlgebraicNormality.lean, line 59.

`AlgebraicNormality.irrational_algebraic_normal_in_some_base`

Open: stated without proof.

The weaker normality conjecture: every irrational algebraic real is normal in at least one integer base b ≥ 2.

theorem irrational_algebraic_normal_in_some_base :
    ∀ x : ℝ, IsIrrationalAlgebraic x → ∃ b : ℕ, 2 ≤ b ∧ IsNormalInBase b x

Category research open; AMS 11 Number theory, 12 Field theory and polynomials, 41 Approximations and expansions. Declared in FormalConjectures/Wikipedia/AlgebraicNormality.lean, line 66.

Sources

LeanAlgebraicNormality.irrational_algebraic_absolutely_normal · AlgebraicNormality.irrational_algebraic_normal_in_some_base

TheoremNon-Power-of-2 Almost Perfect Numbers Conjecture #

References: - Wikipedia - mathworld -

Quoted from FormalConjectures/Wikipedia/AlmostPerfectNumbers.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

`AlmostPerfectNumbers.exists_almost_perfect_not_power_of_two`

Open: stated without proof.

Non-Power-of-2 Almost Perfect Numbers Conjecture. Does there exist an almost perfect number that is not a power of 2?

theorem exists_almost_perfect_not_power_of_two :
    ∃ n : ℕ, AlmostPerfect n ∧ ¬ ∃ k : ℕ, n = 2^k

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AlmostPerfectNumbers.lean, line 48.

Sources

LeanAlmostPerfectNumbers.exists_almost_perfect_not_power_of_two

TheoremThe Alon–Saks–Seymour conjecture (disproved)#

References: * Wikipedia * [GP71] Graham, R. L. and Pollak, H. O. (1971). "On the addressing problem for loop switching." Bell System Tech. J. 50, pp. 2495--2519. * [Ka91] Kahn, J. (1991). "Recent results on some not-so-recent hypergraph matching and covering problems." Extremal problems for finite sets (Visegrád), Bolyai Soc. Math. Stud. 3, pp. 305--353. * [HS12] Huang, H. and Sudakov, B. (2012). "A counterexample to the Alon–Saks–Seymour conjecture and related problems." Combinatorica 32, pp. 205--219. arXiv:1002.4687

Quoted from FormalConjectures/Wikipedia/AlonSaksSeymourConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 3 solved. It also has 1 test statement and 2 API statements, counted here but not shown.

`AlonSaksSeymourConjecture.alon_saks_seymour_conjecture`

Solved: stated here without proof.

The Alon–Saks–Seymour conjecture — disproved.

It was conjectured (Alon, Saks and Seymour, c. 1991, see [Ka91]) that every graph whose edge set is partitioned into \(k\) complete bipartite subgraphs is \((k+1)\)-colourable, i.e. \(\chi(G) \le \operatorname{bp}(G) + 1\) — the natural generalisation of the Graham–Pollak theorem, which is the case \(G = K_n\).

This is false: Huang and Sudakov [HS12] constructed graphs with \(\chi(G) \ge c \operatorname{bp}(G)^{6/5}\).

theorem alon_saks_seymour_conjecture : ¬
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
      G.chromaticNumber ≤ bicliquePartitionNumber G + 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/AlonSaksSeymourConjecture.lean, line 73.

`AlonSaksSeymourConjecture.alon_saks_seymour_conjecture.variants.graham_pollak`

Solved: stated here without proof.

The Graham–Pollak theorem (1971).

The edge set of \(K_n\) cannot be partitioned into fewer than \(n - 1\) complete bipartite subgraphs, and \(n - 1\) suffice: \(\operatorname{bp}(K_n) = n - 1\).

Reference: [GP71].

theorem alon_saks_seymour_conjecture.variants.graham_pollak (n : ℕ) :
    bicliquePartitionNumber (completeGraph (Fin n)) = n - 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/AlonSaksSeymourConjecture.lean, line 87.

`AlonSaksSeymourConjecture.alon_saks_seymour_conjecture.variants.huang_sudakov`

Solved: stated here without proof.

Huang–Sudakov (2012): a polynomial separation.

There is a constant \(c > 0\) and, for every \(k\), a graph \(G\) with \(\operatorname{bp}(G) \le k\) and \(\chi(G) \ge c\,k^{6/5}\).

Reference: [HS12].

theorem alon_saks_seymour_conjecture.variants.huang_sudakov :
    ∃ c : ℝ, 0 < c ∧ ∀ k : ℕ, ∃ (V : Type) (_ : Fintype V) (_ : DecidableEq V)
      (G : SimpleGraph V), bicliquePartitionNumber G ≤ k ∧
        (c * (k : ℝ) ^ ((6 : ℝ) / 5) : ℝ) ≤ (G.chromaticNumber.toNat : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/AlonSaksSeymourConjecture.lean, line 100.

Sources

LeanAlonSaksSeymourConjecture.alon_saks_seymour_conjecture · AlonSaksSeymourConjecture.alon_saks_seymour_conjecture.variants.graham_pollak · AlonSaksSeymourConjecture.alon_saks_seymour_conjecture.variants.huang_sudakov

TheoremAlspach's conjecture on cycle decompositions of complete graphs (1981; proved 2014)#

References: * Wikipedia * [Al81] Alspach, B. (1981). "Research problems, Problem 3." Discrete Math. 36, p. 333. * [BHP14] Bryant, D., Horsley, D. and Pettersson, W. (2014). "Cycle decompositions V: Complete graphs into cycles of arbitrary lengths." Proc. London Math. Soc. 108, pp. 1153--1192. arXiv:1204.3709 * [GJKKO21] Glock, S., Joos, F., Kim, J., Kühn, D. and Osthus, D. (2021). "Resolution of the Oberwolfach problem." J. Eur. Math. Soc. 23, pp. 2511--2547. arXiv:1806.04644

Quoted from FormalConjectures/Wikipedia/AlspachConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 4 research or textbook statements: 1 open and 3 solved. It also has 2 test statements and 1 API statement, counted here but not shown.

`AlspachConjecture.alspach_conjecture`

Solved: stated here without proof.

Alspach's conjecture (1981), proved by Bryant, Horsley and Pettersson (2014).

Let \(n\) be odd and let \(m_1, \dots, m_t\) be integers with \(3 \le m_i \le n\) and \(m_1 + \dots + m_t = \binom{n}{2}\). Then the complete graph \(K_n\) decomposes into cycles of lengths \(m_1, \dots, m_t\). (These conditions are clearly necessary: \(K_n\) has all degrees even only for odd \(n\), and its edges must be split exactly among the cycles.)

theorem alspach_conjecture :
    ∀ (n : ℕ), Odd n → ∀ m : Multiset ℕ, (∀ x ∈ m, 3 ≤ x ∧ x ≤ n) → m.sum = n.choose 2 →
      ∃ C : Multiset (Cycle (completeGraph (Fin n))),
        IsCycleDecomposition (completeGraph (Fin n)) C ∧ lengths C = m

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/AlspachConjecture.lean, line 63.

`AlspachConjecture.alspach_conjecture.variants.even`

Solved: stated here without proof.

The even case (Bryant–Horsley–Pettersson 2014).

For even \(n\), the complete graph minus a perfect matching, \(K_n - I\), decomposes into cycles of lengths \(m_1, \dots, m_t\) whenever \(3 \le m_i \le n\) and \(\sum m_i = \binom{n}{2} - n/2\). Since Mathlib has no canonical perfect matching of \(K_n\), we state this for any perfect matching I.

Reference: [BHP14].

theorem alspach_conjecture.variants.even (n : ℕ) (hn : Even n)
    (I : (completeGraph (Fin n)).Subgraph) (hI : I.IsPerfectMatching)
    (m : Multiset ℕ) (hm : ∀ x ∈ m, 3 ≤ x ∧ x ≤ n) (hsum : m.sum = n.choose 2 - n / 2) :
    ∃ C : Multiset (Cycle (completeGraph (Fin n) \ I.spanningCoe)),
      IsCycleDecomposition (completeGraph (Fin n) \ I.spanningCoe) C ∧ lengths C = m

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/AlspachConjecture.lean, line 81.

`AlspachConjecture.alspach_conjecture.variants.long_cycles`

Solved: stated here without proof.

A long-cycle corollary of the Alspach theorem (Bryant–Horsley–Pettersson 2014).

For odd \(n\), the conjecture holds whenever all the prescribed lengths \(m_i\) are at least \(\lceil(n+4)/2\rceil\). This follows from [BHP14, Theorem 1].

theorem alspach_conjecture.variants.long_cycles (n : ℕ) (hn : Odd n) (m : Multiset ℕ)
    (hm : ∀ x ∈ m, (n + 5) / 2 ≤ x ∧ x ≤ n) (hsum : m.sum = n.choose 2) :
    ∃ C : Multiset (Cycle (completeGraph (Fin n))),
      IsCycleDecomposition (completeGraph (Fin n)) C ∧ lengths C = m

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/AlspachConjecture.lean, line 95.

`AlspachConjecture.alspach_conjecture.variants.oberwolfach`

Open: stated without proof.

The Oberwolfach problem (Ringel 1967).

For odd \(n\) and a \(2\)-regular graph \(F\) on \(n\) vertices, can \(K_n\) be decomposed into \((n-1)/2\) spanning subgraphs isomorphic to \(F\)? The decomposition is known to be impossible for exactly two pairs with odd \(n\) — \((9, C_4 + C_5)\) and \((11, C_3 + C_3 + C_5)\) — and is conjectured to exist in every other case. Known for all sufficiently large \(n\) [GJKKO21].

theorem alspach_conjecture.variants.oberwolfach :
    ∀ (n : ℕ), Odd n → 3 ≤ n →
      ∀ (F : SimpleGraph (Fin n)) [DecidableRel F.Adj], (∀ v, F.degree v = 2) →
      IsEmpty (F ≃g oberwolfachException9) → IsEmpty (F ≃g oberwolfachException11) →
      ∃ D : Fin ((n - 1) / 2) → SimpleGraph (Fin n),
        (∀ i, Nonempty (D i ≃g F)) ∧
        ∀ u v, (completeGraph (Fin n)).Adj u v ↔ ∃! i, (D i).Adj u v

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/AlspachConjecture.lean, line 183.

Sources

LeanAlspachConjecture.alspach_conjecture · AlspachConjecture.alspach_conjecture.variants.even · AlspachConjecture.alspach_conjecture.variants.long_cycles · AlspachConjecture.alspach_conjecture.variants.oberwolfach

TheoremAmicable numbers #

Two distinct positive integers form an amicable pair if each equals the sum of the proper divisors of the other. Equivalently, \((a, b)\) is an amicable pair if \(\sigma(a) = a + b\) and \(\sigma(b) = a + b\), where \(\sigma(n)\) denotes the sum of all positive divisors of \(n\).

Several open problems about amicable numbers are formalised here:

Do there exist relatively prime amicable numbers?

Are there infinitely many amicable pairs?

Do there exist amicable numbers with opposite parity (one even, one odd)?

References: - Wikipedia - MathWorld - OEIS A063990

Quoted from FormalConjectures/Wikipedia/AmicableNumbers.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 3 open. It also has 2 test statements, counted here but not shown.

`AmicableNumbers.relatively_prime_amicable`

Open: stated without proof.

Relatively prime amicable numbers conjecture. Do there exist amicable numbers \((a, b)\) with \(\gcd(a, b) = 1\)?

All known amicable pairs share a common factor. It is an open question whether a pair of relatively prime amicable numbers can exist.

Reference: Wikipedia

theorem relatively_prime_amicable :
    ∃ a b : ℕ, IsAmicable a b ∧ a ≠ b ∧ a.Coprime b

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AmicableNumbers.lean, line 66.

`AmicableNumbers.infinitely_many_amicable`

Open: stated without proof.

Infinitely many amicable numbers conjecture.

Are there infinitely many pairs of amicable numbers?

While many amicable pairs are known, it remains open whether there are infinitely many.

Reference: Wikipedia, erdosproblems.com/830

theorem infinitely_many_amicable : type_of% Erdos830.erdos_830.parts.i

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AmicableNumbers.lean, line 81.

`AmicableNumbers.opposite_parity_amicable`

Open: stated without proof.

Amicable numbers with opposite parity conjecture. Do there exist amicable numbers \((a, b)\) where one is even and the other is odd?

All known amicable pairs are either both even or both odd. It is widely believed that mixed-parity amicable pairs do not exist, but this remains open.

Reference: Wikipedia

theorem opposite_parity_amicable :
    ∃ a b : ℕ, IsAmicable a b ∧ (Even a ↔ Odd b)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/AmicableNumbers.lean, line 94.

Sources

LeanAmicableNumbers.relatively_prime_amicable · AmicableNumbers.infinitely_many_amicable · AmicableNumbers.opposite_parity_amicable

TheoremThe Andrews-Curtis conjecture #

The conjecture says that every normally generating n-tuple in the free group on n generators is Andrews-Curtis equivalent to the standard free basis.

References:

Wikipedia, Andrews-Curtis conjecture

A. D. Myasnikov, A. G. Myasnikov and V. Shpilrain, On the Andrews-Curtis equivalence

Quoted from FormalConjectures/Wikipedia/AndrewsCurtis.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

`AndrewsCurtis.andrews_curtis_conjecture`

Open: stated without proof.

The Andrews-Curtis conjecture.

Every normally generating n-tuple in the free group of rank n is Andrews-Curtis equivalent to the standard tuple of free generators.

theorem andrews_curtis_conjecture (n : ℕ) (r : RelatorTuple n)
    (hr : NormallyGenerates r) :
    Equivalent r (standardRelators n)

Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/AndrewsCurtis.lean, line 77.

Sources

LeanAndrewsCurtis.andrews_curtis_conjecture

TheoremAndrica's conjecture #

References: - Wikipedia - Luan Alberto Ferreira, Real exponential sums over primes and prime gaps

Quoted from FormalConjectures/Wikipedia/Andrica.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 1 open and 1 solved.

`Andrica.andrica_conjecture`

Open: stated without proof.

Andrica's conjecture The inequality \(\sqrt{p_{n+1}}-\sqrt{p_n} < 1\) holds for all \(n\), where \(p_n\) is the \(n\)-th prime number.

theorem andrica_conjecture (n : ℕ) :
    Real.sqrt ((n+1).nth Nat.Prime) - Real.sqrt (n.nth Nat.Prime) < 1

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Andrica.lean, line 38.

`Andrica.andrica_conjecture.ferreira_large_n`

Solved: stated here without proof.

Ferreira proved that Andrica's conjecture is true for sufficiently large n.

theorem andrica_conjecture.ferreira_large_n :
    ∀ᶠ n in atTop, Real.sqrt ((n+1).nth Nat.Prime) - Real.sqrt (n.nth Nat.Prime) < 1

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Andrica.lean, line 46.

Sources

LeanAndrica.andrica_conjecture · Andrica.andrica_conjecture.ferreira_large_n

TheoremArtin's conjecture on primitive roots #

Artin's conjecture predicts, given an integer \(a\), densities of primes \(p\) for which \(a\) is a primitive root modulo \(p\). Under certain conditions (when \(a\) is not a power and its squarefree part is not \(1\pmod{4}\)) the density is given by Artin's constant

\[\prod_{p\ \text{prime}} \left(1 - \frac{1}{p(p - 1)}\right).\]

For more general values of \(a\), this constant must be corrected by certain factors. - When \(a = b^m\), \(m\) is a maximal odd power, the squarefree part of \(b\) satisfies \(b_0 \not\equiv 1\pmod{4}\). Then Artin's constant should be multiplied by

\[\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}.\]

When \(a = b^m\), \(m\) is a maximal power, the squarefree part of \(b\) satisfies \(b_0\equiv 1\pmod{4}\). Then Artin's constant should be multiplied by the factor in the above bullet, as well as an additional entanglement factor from the primes dividing \(\gcd(b_0, m)\) and primes dividing \(b_0\):

\[1 - \prod_{p \mid \gcd(b_0, m)} \frac{1}{2 - p} \prod_{p \mid b_0, p\nmid m} \frac{1}{1 + p - p^2}.\]

When \(a = -1\) or \(a\) is a square, then the density is \(0\).

Note that Artin's conjecture has been proved by Hooley [Ho67] subject to the Riemann hypothesis for the Dedekind zeta functions of the Kummer fields \(\mathbb{Q}(\zeta_k, a^{1/k})\), \(k\) squarefree. These fields are in general non-abelian over \(\mathbb{Q}\), so this hypothesis is not covered by the Generalized Riemann Hypothesis for Dirichlet \(L\)-functions.

References: - Wikipedia - A85397 - LMS14 Lenstra, H.W. et al. "Character sums for primitive root densities" arXiv:1112.4816 [math.NT] (2014). - [Ho67] Hooley, C. "On Artin's conjecture." Journal für die reine und angewandte Mathematik 225 (1967): 209-220.

Quoted from FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 9 research or textbook statements: 4 open and 5 solved. It also has 1 API statement, counted here but not shown.

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.i`

Open: stated without proof.

Artin's Conjecture on Primitive Roots, first half. Let \(a\) be an integer that is not a square number and not \(−1\). Then the set \(S(a)\) of primes \(p\) such that \(a\) is a primitive root modulo \(p\) has a positive asymptotic density inside the set of primes. In particular, \(S(a)\) is infinite.

theorem artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ -1) :
    ∃ x > 0, (S a).HasDensity x {p | p.Prime}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 120.

`ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.i`

Solved: stated here without proof.

Artin's Conjecture on Primitive Roots, first half, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields \(\mathbb{Q}(\zeta_k, a^{1/k})\), \(k\) squarefree [Ho67].

theorem conditional_artin_primitive_roots.parts.i (a : ℤ) (ha : ¬IsSquare a) (ha' : a ≠ -1)
    (h : HooleyHypothesis a) :
    ∃ x > 0, (S a).HasDensity x {p | p.Prime}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 130.

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.ii`

Open: stated without proof.

Artin's Conjecture on Primitive Roots, second half. Write \(a = a_0 b^2\) where \(a_0\) is squarefree. Under the conditions that \(a\) is not a perfect power and \(a_0\not\equiv 1\pmod{4}\) (sequence A85397 in the OEIS), the density of the set \(S(a)\) of primes \(p\) such that \(a\) is a primitive root modulo \(p\) is independent of \(a\) and equals Artin's constant.

theorem artin_primitive_roots.parts.ii
    (a a_0 b : ℤ) (ha : a = a_0 * b ^ 2)
    (ha' : ∀ n m, m ≠ 1 → a ≠ n ^ m) (ha_0 : Squarefree a_0)
    (ha_0' : ¬a_0 ≡ 1 [ZMOD 4]) :
    (S a).HasDensity ArtinConstant {p | p.Prime}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 143.

`ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.ii`

Solved: stated here without proof.

Artin's Conjecture on Primitive Roots, second half, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields \(\mathbb{Q}(\zeta_k, a^{1/k})\), \(k\) squarefree [Ho67].

theorem conditional_artin_primitive_roots.parts.ii
    (a a_0 b : ℤ) (ha : a = a_0 * b ^ 2)
    (ha' : ∀ n m, m ≠ 1 → a ≠ n ^ m) (ha_0 : Squarefree a_0)
    (ha_0' : ¬a_0 ≡ 1 [ZMOD 4])
    (h : HooleyHypothesis a) :
    (S a).HasDensity ArtinConstant {p | p.Prime}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 157.

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_square_or_minus_one`

Proved here.

Artin's Conjecture on Primitive Roots, second half, different residue version If \(a\) is a square number or \(a = −1\), then the density of the set \(S(a)\) of primes \(p\) such that \(a\) is a primitive root modulo \(p\) is \(0\).

theorem artin_primitive_roots.variants.part_ii_square_or_minus_one
    (a : ℤ) (ha : IsSquare a ∨ a = -1) :
    (S a).HasDensity 0 {p | p.Prime}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 198.

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one`

Open: stated without proof.

Artin's Conjecture on Primitive Roots, second half, power version If \(a = b^m\) is a perfect odd power of a number \(b\) whose squarefree part \(b_0\not\equiv 1 \pmod{4}\), then the density of the set \(S(a)\) of primes \(p\) such that \(a\) is a primitive root modulo \(p\) is given by

\[C\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}\]

, where \(C\) is Artin's constant.

theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one
    (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v^u) (hm₁ : 1 < m)
    (hm₂ : Odd m) (hb' : ¬ b.squarefreePart ≡ 1 [MOD 4]) :
    (S a).HasDensity (ArtinConstant * powCorrectionFactor m) {p | p.Prime}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 214.

`ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one`

Solved: stated here without proof.

Artin's Conjecture on Primitive Roots, second half, power version, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields \(\mathbb{Q}(\zeta_k, a^{1/k})\), \(k\) squarefree [Ho67].

theorem conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one
    (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m)
    (hm₂ : Odd m) (hb' : ¬ b.squarefreePart ≡ 1 [MOD 4])
    (h : HooleyHypothesis a) :
    (S a).HasDensity (ArtinConstant * powCorrectionFactor m) {p | p.Prime}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 226.

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one`

Open: stated without proof.

Artin's Conjecture on Primitive Roots, second half, power version If \(a = b^m\) is a perfect power of a number \(b\) whose squarefree part \(b_0\equiv 1 \pmod{4}\), then the density of the set \(S(a)\) of primes \(p\) such that \(a\) is a primitive root modulo \(p\) is given by

\[C \left(\prod_{p \mid m} \frac{p(p-2)}{(p ^ 2 - p - 1)}\right) \left(1 - \prod_{p \mid \gcd(b_0, m)} \frac{1}{2 - p} \prod_{p \mid b_0, p\nmid m} \frac{1}{(1 + p - p ^ 2)}\right),\]

where \(C\) is Artin's constant.

theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one
    (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m)
    (hm₂ : Odd m) (hb' : b.squarefreePart ≡ 1 [MOD 4]) :
    (S a).HasDensity
      (ArtinConstant * powCorrectionFactor m * entanglementFactor b m)
      {p | p.Prime}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 244.

`ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one`

Solved: stated here without proof.

Artin's Conjecture on Primitive Roots, second half, power version, conditional on the Riemann hypothesis for the Dedekind zeta functions of the fields \(\mathbb{Q}(\zeta_k, a^{1/k})\), \(k\) squarefree [Ho67].

theorem conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one
    (a m b : ℕ) (ha : a = b ^ m) (hb : ∀ u v, 1 < u → b ≠ v ^ u) (hm₁ : 1 < m)
    (hm₂ : Odd m) (hb' : b.squarefreePart ≡ 1 [MOD 4])
    (h : HooleyHypothesis a) :
    (S a).HasDensity
      (ArtinConstant * powCorrectionFactor m * entanglementFactor b m)
      {p | p.Prime}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ArtinPrimitiveRootsConjecture.lean, line 258.

Sources

TheoremBalanced prime conjecture #

References: - Wikipedia - OEIS A6562

Quoted from FormalConjectures/Wikipedia/BalancedPrimes.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 2 open.

`BalancedPrimes.balanced_primes`

Open: stated without proof.

Let \(p_k\) be the \(k\)-th prime number. Are there infinitely many \(n\) such that \((p_n + p_{n+2}) / 2\) is prime?

theorem balanced_primes :
    {n : ℕ | Prime ((Nat.nth Prime n + Nat.nth Prime (n + 2)) / 2)}.Infinite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/BalancedPrimes.lean, line 37.

`BalancedPrimes.balanced_primes_order`

Open: stated without proof.

Let \(p_k\) be the \(k\)-th prime number. Are there infinitely many \(n\) such that \(p_n = \dfrac{\sum_{i = 1} ^ k p_{n - i} + p_{n + i}}{2*k}\)?

theorem balanced_primes_order :
    ∀ k > 0, {n : ℕ | k ≤ n ∧ 2 * k * Nat.nth Prime n = ∑ i ∈ .Ioc 0 k,
      ((n - i).nth Prime + (n + i).nth Prime)}.Infinite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/BalancedPrimes.lean, line 47.

Sources

LeanBalancedPrimes.balanced_primes · BalancedPrimes.balanced_primes_order

TheoremBateman-Horn Conjecture #

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/BatemanHornConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

`BatemanHornConjecture.bateman_horn_conjecture`

Open: stated without proof.

The Bateman-Horn Conjecture Given a finite collection of distinct irreducible polynomials non-constant \(f_1, f_2, \dots, f_k \in \mathbb{Z}[x]\) with positive leading coefficients that satisfy the Schinzel condition, the number of positive integers \(n \leq x\) for which all polynomials \(f_i\) are simultaneously prime is asymptotic to:

\[\frac{C}{D} \frac{x}{(\log x)^k}\]

where \(D = \prod_i \deg(f_i)\) and \(C\) is the Bateman-Horn constant given by the convergent infinite product:

\[C = \prod_{p\in\mathbb{P}} (1 - 1/p)^{-k} (1 - \omega_p/p)\]

Here \(\omega_p\) is the number of residue classes modulo \(p\) for which at least one polynomial vanishes. The product is only conditionally convergent: it is the limit as \(N \to \infty\) of the partial products over the primes \(p < N\).

The Schinzel condition ensures that for each prime \(p\), there exists some integer \(n\) such that \(p\) does not divide the product \(f_1(n) f_2(n) \dotsb f_k(n)\), which guarantees the infinite product converges to a positive value.

theorem bateman_horn_conjecture
    (polys : Finset ℤ[X])
    (h_nonempty : polys.Nonempty)
    (h_irreducible : ∀ f ∈ polys, BunyakovskyCondition f)
    (h_compat : SchinzelCondition polys) :
    ∃ C : ℝ, 0 < C ∧ Tendsto (BatemanHornPartialProduct polys) atTop (𝓝 C) ∧
      (fun x : ℝ => (CountSimultaneousPrimes polys x : ℝ)) ~[atTop]
        (fun x : ℝ => C / DegreesProduct polys * x / (Real.log x) ^ polys.card)

Category research open; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/BatemanHornConjecture.lean, line 82.

Sources

LeanBatemanHornConjecture.bateman_horn_conjecture

TheoremBeal conjecture #

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/BealConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 1 open and 1 textbook result.

`BealConjecture.beal_conjecture`

Open: stated without proof.

The Beal Conjecture: if we are given positive integers \(A, B, C, x, y, z\) such that \(x, y, z > 2\) and \(A^x + B^y = C^z\) then \(A, B, C\) have a common divisor.

theorem beal_conjecture : bealConjecture

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/BealConjecture.lean, line 39.

`BealConjecture.flt_of_beal_conjecture`

Textbook result, proved here.

The Beal Conjecture implies Fermat's last theorem

theorem flt_of_beal_conjecture (H : bealConjecture) :
    FermatLastTheorem

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/BealConjecture.lean, line 46.

Sources

LeanBealConjecture.beal_conjecture · BealConjecture.flt_of_beal_conjecture

TheoremBeck–Fiala theorem and conjecture #

Discrepancy of bounded-degree set systems. Given sets \(S_1, \dots, S_m \subseteq [n]\) such that every element of \([n]\) belongs to at most \(t\) of the sets (the system has degree at most \(t\)), one seeks a colouring \(\chi \colon [n] \to \{-1, +1\}\) making every set as balanced as possible, i.e. minimizing the discrepancy \(\max_i \left|\sum_{j \in S_i} \chi(j)\right|\).

The Beck–Fiala theorem (1981) states that every set system of degree at most \(t \ge 1\) has discrepancy at most \(2t - 1\). The Beck–Fiala conjecture asserts that the truth is much stronger: the discrepancy of a degree-\(t\) system is \(O(\sqrt{t})\), with a constant independent of \(n\), \(m\) and \(t\).

Despite considerable attention the bound \(2t - 1\) has been improved only slightly: Bukh (2016) proved a bound of the form \(2t - \log^* t\) (where \(\log^*\) is the iterated logarithm), and Banaszczyk's vector balancing theorem yields \(O(\sqrt{t \log n})\). The Komlós conjecture (see KomlosConjecture.lean) would imply the Beck–Fiala conjecture, since scaling the incidence vectors of a degree-\(t\) system by \(1/\sqrt{t}\) produces vectors of Euclidean norm at most \(1\).

References: - Wikipedia - J. Beck and T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981), 1–8 - B. Bukh, An improvement of the Beck–Fiala theorem, Combinatorics, Probability and Computing 25 (2016), 380–398 - W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998), 351–360

Quoted from FormalConjectures/Wikipedia/BeckFialaConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 test statement, counted here but not shown.

`BeckFiala.beck_fiala_theorem`

Solved: stated here; a Lean proof is at https://github.com/Lemmy00/beck-fiala-lean/blob/19334973121b07e428c51e15b914e9ca4921fbb9/BeckFialaProof/BeckFiala.lean#L35.

The Beck–Fiala theorem

If \(S_1, \dots, S_m \subseteq [n]\) is a set system of degree at most \(t\), i.e. every \(j \in [n]\) lies in at most \(t\) of the sets, and \(t \ge 1\), then there is a colouring \(\chi \colon [n] \to \{-1, +1\}\) with \(\left|\sum_{j \in S_i} \chi(j)\right| \le 2t - 1\) for every \(i\).

The hypothesis \(t \ge 1\) is necessary: a system of degree \(0\) consists of empty sets only, whose discrepancy is \(0 > 2 \cdot 0 - 1\).

[J. Beck and T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981), 1–8.]

theorem beck_fiala_theorem (n m t : ℕ) (ht : 1 ≤ t) (S : Fin m → Finset (Fin n))
    (hdeg : ∀ j, (Finset.univ.filter fun i => j ∈ S i).card ≤ t) :
    ∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧
      ∀ i, |∑ j ∈ S i, χ j| ≤ 2 * (t : ℝ) - 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/BeckFialaConjecture.lean, line 73.

`BeckFiala.beck_fiala_conjecture`

Open: stated without proof.

The Beck–Fiala conjecture

There exists a universal constant \(C > 0\) such that every set system \(S_1, \dots, S_m \subseteq [n]\) of degree at most \(t\) admits a colouring \(\chi \colon [n] \to \{-1, +1\}\) with \(\left|\sum_{j \in S_i} \chi(j)\right| \le C \sqrt{t}\) for every \(i\).

theorem beck_fiala_conjecture :
    ∃ C : ℝ, 0 < C ∧ ∀ (n m t : ℕ) (S : Fin m → Finset (Fin n)),
      (∀ j, (Finset.univ.filter fun i => j ∈ S i).card ≤ t) →
      ∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧
        ∀ i, |∑ j ∈ S i, χ j| ≤ C * Real.sqrt t

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/BeckFialaConjecture.lean, line 88.

Sources

LeanBeckFiala.beck_fiala_theorem · BeckFiala.beck_fiala_conjecture

TheoremThe Berge–Fulkerson conjecture #

References: * Wikipedia * [Fu71] Fulkerson, D. R. (1971). "Blocking and anti-blocking pairs of polyhedra." Math. Programming 1, pp. 168--194. * [Se79] Seymour, P. D. (1979). "On multi-colourings of cubic graphs, and conjectures of Fulkerson and Tutte." Proc. London Math. Soc. 38, pp. 423--460. * [Ma11] Mazzuoccolo, G. (2011). "The equivalence of two conjectures of Berge and Fulkerson." J. Graph Theory 68, pp. 125--128. * [FR94] Fan, G. and Raspaud, A. (1994). "Fulkerson's conjecture and circuit covers." J. Combin. Theory Ser. B 61, pp. 133--138. * [Pe91] Petersen, J. (1891). "Die Theorie der regulären graphs." Acta Math. 15, pp. 193--220.

Quoted from FormalConjectures/Wikipedia/BergeFulkersonConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 4 research or textbook statements: 3 open and 1 solved. It also has 1 API statement, counted here but not shown.

`BergeFulkersonConjecture.berge_fulkerson_conjecture`

Open: stated without proof.

The Berge–Fulkerson conjecture (Fulkerson 1971).

Every bridgeless cubic graph has six perfect matchings such that every edge lies in exactly two of them.

theorem berge_fulkerson_conjecture :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      IsCubic G → G.IsBridgeless →
      ∃ M : Fin 6 → G.Subgraph, IsPerfectMatchingCover G 6 2 M

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/BergeFulkersonConjecture.lean, line 64.

`BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.berge`

Open: stated without proof.

Berge's conjecture: five perfect matchings covering every edge.

Every bridgeless cubic graph has five perfect matchings whose union is the whole edge set. Mazzuoccolo [Ma11] proved this to be equivalent to the Berge–Fulkerson conjecture.

Reference: [Ma11].

theorem berge_fulkerson_conjecture.variants.berge :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      IsCubic G → G.IsBridgeless →
      ∃ M : Fin 5 → G.Subgraph, (∀ i, (M i).IsPerfectMatching) ∧
        ∀ e ∈ G.edgeSet, ∃ i, e ∈ (M i).edgeSet

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/BergeFulkersonConjecture.lean, line 79.

`BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.fan_raspaud`

Open: stated without proof.

The Fan–Raspaud conjecture (1994).

Every bridgeless cubic graph has three perfect matchings with no edge common to all three. This would follow from the Berge–Fulkerson conjecture.

Reference: [FR94].

theorem berge_fulkerson_conjecture.variants.fan_raspaud :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      IsCubic G → G.IsBridgeless →
      ∃ M : Fin 3 → G.Subgraph, (∀ i, (M i).IsPerfectMatching) ∧
        ∀ e, ¬ (e ∈ (M 0).edgeSet ∧ e ∈ (M 1).edgeSet ∧ e ∈ (M 2).edgeSet)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/BergeFulkersonConjecture.lean, line 95.

`BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.petersen`

Solved: stated here without proof.

Petersen's theorem (1891): every bridgeless cubic graph has a perfect matching.

This is the case of a single perfect matching, and is the starting point for all of the above.

Reference: [Pe91].

theorem berge_fulkerson_conjecture.variants.petersen
    {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hcubic : IsCubic G) (hbridgeless : G.IsBridgeless) :
    ∃ M : G.Subgraph, M.IsPerfectMatching

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/BergeFulkersonConjecture.lean, line 111.

Sources

LeanBergeFulkersonConjecture.berge_fulkerson_conjecture · BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.berge · BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.fan_raspaud · BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.petersen

TheoremBetrothed numbers #

References: - Wikipedia - OEIS A005276

Quoted from FormalConjectures/Wikipedia/BetrothedNumbers.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 2 open. It also has 2 test statements, counted here but not shown.

`BetrothedNumbers.same_parity_betrothed`

Open: stated without proof.

Same parity betrothed numbers conjecture. Do there exist betrothed numbers \((m, n)\) where both have the same parity (both even or both odd)?

All known betrothed pairs consist of one even and one odd number.

The requirement \(m \neq n\) is part of the question: \(\mathrm{IsBetrothed}\ n\ n\) says \(\sigma(n) = 2n + 1\), i.e. that \(n\) is quasiperfect, which is the separate open problem QuasiperfectNumbers.exists_quasiperfect.

theorem same_parity_betrothed :
    ∃ m n : ℕ, m ≠ n ∧ IsBetrothed m n ∧ (Even m ↔ Even n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/BetrothedNumbers.lean, line 67.

`BetrothedNumbers.infinitely_many_betrothed`

Open: stated without proof.

Infinitude of betrothed numbers conjecture. Are there infinitely many betrothed number pairs?

theorem infinitely_many_betrothed :
    {p : ℕ × ℕ | p.1 < p.2 ∧ IsBetrothed p.1 p.2}.Infinite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/BetrothedNumbers.lean, line 77.

Sources

LeanBetrothedNumbers.same_parity_betrothed · BetrothedNumbers.infinitely_many_betrothed

TheoremThe Bing-Borsuk Conjecture #

The Bing-Borsuk conjecture states that every \(n\)-dimensional homogeneous absolute neighborhood retract is a topological \(n\)-manifold.

The conjecture has been verified in dimensions \(1\) and \(2\) but remains open in higher dimensions. A notable consequence is that if the \(3\)-dimensional case is true, it implies the Poincaré conjecture.

References: - Wikipedia - [HR2008] Halverson, Denise M., and Dušan Repovš. "The Bing-Borsuk and the Busemann conjectures." Mathematical Communications 13.2 (2008): 163-184. https://arxiv.org/abs/0811.0886

Quoted from FormalConjectures/Wikipedia/BingBorsuk.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

`BingBorsuk.bing_borsuk_conjecture`

Open: stated without proof.

The Bing-Borsuk Conjecture: every \(n\)-dimensional homogeneous absolute neighborhood retract is a topological \(n\)-manifold. A topological space \(X\) is an \(n\)-dimensional manifold when T2Space X ∧ Nonempty (ChartedSpace (Fin n → ℝ) X). The hypothesis [MetrizableSpace X] implies T2Space X so this does not appear in the conclusion.

theorem bing_borsuk_conjecture : ∀ n : ℕ, ∀ (X : Type) [TopologicalSpace X] [MetrizableSpace X] [HomogeneousSpace X] [IsAbsoluteNeighborhoodRetract X],
    HasLebesgueCoveringDimensionEq X n → Nonempty (ChartedSpace (Fin n → ℝ) X)

Category research open; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Wikipedia/BingBorsuk.lean, line 51.

Sources

LeanBingBorsuk.bing_borsuk_conjecture

TheoremBloch and Landau constants #

References: - Wikipedia - [CP96] Chen, H., Gauthier, P. M. "On Bloch's constant." Journal d'Analyse Mathématique 69 (1996), 275–291. - [AG37] Ahlfors, L. V., Grunsky, H. "Über die Blochsche Konstante." Mathematische Zeitschrift 42 (1937), 671–673. - [Ya95] Yanagihara, H. "On the locally univalent Bloch constant." Journal d'Analyse Mathématique 65 (1995), 1–17. - [Ra43] Rademacher, H. "On the Bloch-Landau Constant."" American Journal of Mathematics 65 (1943), 387–390. - OptimizationConstants - [Skin2009] Skinner, Brian. The univalent Bloch constant problem. Complex Variables and Elliptic Equations 54 (2009), no. 10, 951–955. - MathWorld - Bhowmik–Sen - [Re2008] Rettinger, R. "Bloch's constant is computable." Journal of Universal Computer Science 14 (2008), 896–907. In particular, a schlicht disk is the image of a subdomain under a biholomorphic restriction.

Quoted from FormalConjectures/Wikipedia/Bloch.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 8 research or textbook statements: 2 open and 6 solved. It also has 4 API statements, counted here but not shown.

`Bloch.blochConstant_lower_bound`

Solved: stated here without proof.

It is proved in [CP96] that the Bloch constant is bounded below by \(\sqrt{3}/4 + 2 \times 10^{-4}\)

theorem blochConstant_lower_bound : Real.sqrt 3 / 4 + 2 * 10 ^ (-4 : ℤ) ≤ blochConstant

Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Bloch.lean, line 136.

`Bloch.blochConstant_upper_bound`

Solved: stated here without proof.

It is proved in [AG37] that the Bloch constant is bounded above by \(\frac{1}{\sqrt{1 + \sqrt{3}}}\frac{\Gamma(1/3) \Gamma(11/12)}{\Gamma(1/4)}\).

theorem blochConstant_upper_bound :
    blochConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (11 / 12) /
    (Real.Gamma (1 / 4) * Real.sqrt (1 + Real.sqrt 3))

Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Bloch.lean, line 142.

`Bloch.blochConstant_exact_value`

Open: stated without proof.

Ahlfors and Grunsky also conjectured in [AG37] that this upper bound is the precise value of the Bloch constant.

theorem blochConstant_exact_value :
    blochConstant = Real.Gamma (1 / 3) * Real.Gamma (11 / 12) /
    (Real.Gamma (1 / 4) * Real.sqrt (1 + Real.sqrt 3))

Category research open; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Bloch.lean, line 150.

`Bloch.univalentBlochConstant_lower_bound`

Solved: stated here without proof.

It is proved in [Skin2009] that the Univalent Bloch constant is bounded below by \(0.5708858\).

theorem univalentBlochConstant_lower_bound : 0.5708858 ≤ univalentBlochConstant

Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Bloch.lean, line 166.

`Bloch.univalentBlochConstant_upper_bound`

Proved here.

The Univalent Bloch constant is trivially bounded above by the Bloch radius of the identity function, which is \(1\). This is the best upper bound we know according to [OptimizationConstants].

theorem univalentBlochConstant_upper_bound : univalentBlochConstant ≤ 1

Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Bloch.lean, line 172.

`Bloch.landauConstant_lower_bound`

Solved: stated here without proof.

It is proved in [Ya95] that the Landau constant is bounded below by \(0.5 + 10 ^ {-335}\).

theorem landauConstant_lower_bound : 0.5 + 10 ^ (-335 : ℤ) ≤ landauConstant

Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Bloch.lean, line 194.

`Bloch.landauConstant_upper_bound`

Solved: stated here without proof.

It is proved in [Ra43] that the Landau constant is bounded above by \(\frac{1}{\sqrt{1 + \sqrt{3}}}\frac{\Gamma(1/3) \Gamma(5/6)}{\Gamma(1/6)}\).

theorem landauConstant_upper_bound :
    landauConstant ≤ Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6)

Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Bloch.lean, line 200.

`Bloch.landauConstant_exact_value`

Open: stated without proof.

In [Ra43], Rademacher says that he strongly believed that this upper bound is the precise value of the Landau constant.

theorem landauConstant_exact_value :
    landauConstant = Real.Gamma (1 / 3) * Real.Gamma (5 / 6) / Real.Gamma (1 / 6)

Category research open; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Bloch.lean, line 207.

Sources

LeanBloch.blochConstant_lower_bound · Bloch.blochConstant_upper_bound · Bloch.blochConstant_exact_value · Bloch.univalentBlochConstant_lower_bound · Bloch.univalentBlochConstant_upper_bound · Bloch.landauConstant_lower_bound · Bloch.landauConstant_upper_bound · Bloch.landauConstant_exact_value

TheoremBorsuk's conjecture #

In 1933 Karol Borsuk [Bo33] asked whether every bounded subset of \(\mathbb{R}^n\) can be partitioned into \(n + 1\) sets, each of strictly smaller diameter. The hypothesis that the answer is positive became known as Borsuk's conjecture.

The conjecture is true for \(n = 2\) [Bo33] and \(n = 3\) [Pe47, Eg55]. It is false in general: Kahn and Kalai [KK93] disproved it for \(n = 1325\) and for all \(n > 2014\). Bondarenko [Bo14] gave a counterexample in dimension \(65\), and Jenrich and Brouwer [JB14] one in dimension \(64\), the smallest refereed counterexample. In 2026 Grinsztajn [Gr26] posted a 321-point counterexample in dimension \(63\), obtained with AI assistance and verified by exact computation; the same configuration was found independently by Konz and by Ji [Ji26]. In September 2026 an internal OpenAI model gave a compact counterexample in dimension \(9\) [OAI26]: the set of rank-one orthogonal projectors on \(\mathbb{R}^4\), viewed in the nine-dimensional affine space of trace-one symmetric \(4 \times 4\) matrices with the Frobenius metric, has diameter \(\sqrt{2}\) and cannot be covered by \(10\) sets of smaller diameter. The paper extends this to every dimension \(n \geq 9\) (Corollary 7.1); see borsuk_conjecture.not_of_nine_le. The linked Lean proof establishes the case \(n = 9\). The cases \(4 \leq n \leq 8\) are open. In dimension \(4\), every bounded set can be partitioned into \(9\) parts of smaller diameter [La82], and a 2026 preprint reduces this to \(8\) parts [TV26].

Erdős Problem 505 (FormalConjectures.ErdosProblems.«505») points to this file.

References: - Wikipedia - [Bo33] Borsuk, K. (1933). Drei Sätze über die n-dimensionale euklidische Sphäre. Fundamenta Mathematicae 20, 177–190. https://doi.org/10.4064/fm-20-1-177-190 - [Pe47] Perkal, J. (1947). Sur la subdivision des ensembles en parties de diamètre inférieur. Colloquium Mathematicum 2, 45. - [Eg55] Eggleston, H. G. (1955). Covering a three-dimensional set with sets of smaller diameter. Journal of the London Mathematical Society 30, 11–24. https://doi.org/10.1112/jlms/s1-30.1.11 - [La82] Lassak, M. (1982). An estimate concerning Borsuk partition problem. Bulletin of the Polish Academy of Sciences, Mathematics 30(9–10), 449–451. - [KK93] Kahn, J., Kalai, G. (1993). A counterexample to Borsuk's conjecture. Bulletin of the American Mathematical Society 29(1), 60–62. https://arxiv.org/abs/math/9307229 - [Bo14] Bondarenko, A. (2014). On Borsuk's conjecture for two-distance sets. Discrete & Computational Geometry 51(3), 509–515. https://doi.org/10.1007/s00454-014-9579-4 - [JB14] Jenrich, T., Brouwer, A. E. (2014). A 64-dimensional counterexample to Borsuk's conjecture. Electronic Journal of Combinatorics 21(4), P4.29. https://doi.org/10.37236/4069 - [Gr26] Grinsztajn, M. (2026). A 63-dimensional counterexample to Borsuk's conjecture. Proof note and verification script, https://github.com/maaxgrin/borsuk-63-counterexample - [Ji26] Ji, Y. (2026). An AI generated counterexample to Borsuk problem in dimension 63. https://arxiv.org/abs/2608.12561 (withdrawn as a duplicate of [Gr26]) - [TV26] Tolmachev, A., Voronov, V. (2026). Reducing the upper bound for the Borsuk number in \(\mathbb{R}^4\) to 8. https://arxiv.org/abs/2605.19068 - [OAI26] OpenAI (2026). A nine-dimensional counterexample to Borsuk's covering assertion. OpenAI Math Release preprint. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026/paper.pdf - [OP28a] Tao, T. et al., Optimization problems, constant 28a (smallest Borsuk counterexample dimension). https://teorth.github.io/optimizationproblems/constants/28a.html - [Ka15] Kalai, G. (2015). Some old and new problems in combinatorial geometry I: Around Borsuk's problem. https://arxiv.org/abs/1505.04952

Quoted from FormalConjectures/Wikipedia/BorsukConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 13 research or textbook statements: 1 open, 11 solved and 1 textbook result. It also has 1 test statement and 1 API statement, counted here but not shown.

`Borsuk.borsuk_conjecture`

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Geometry/Borsuk/Main.lean#L117.

Borsuk's conjecture fails in the formerly open range \(4 \leq n \leq 62\): it is not the case that every bounded subset of \(\mathbb{R}^n\) with at least two points can be partitioned into \(n + 1\) sets of strictly smaller diameter for every such \(n\).

The conjecture is true for \(n \leq 3\) and false for \(n \geq 9\). It was disproved in dimension \(9\) by an internal OpenAI model in September 2026 [OAI26]; see borsuk_conjecture.not_nine and the linked Lean proof. The cases \(4 \leq n \leq 8\) remain open.

theorem borsuk_conjecture : ¬ ∀ n, 4 ≤ n → n ≤ 62 → BorsukConjecture n

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 141.

`Borsuk.borsuk_conjecture.four`

Open: stated without proof.

Borsuk's conjecture in dimension \(4\), the smallest open case.

theorem borsuk_conjecture.four : BorsukConjecture 4

Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 146.

`Borsuk.borsuk_conjecture.four.nine_parts`

Solved: stated here without proof.

Partial result in dimension \(4\): every bounded subset of \(\mathbb{R}^4\) with at least two points can be partitioned into \(9\) sets of strictly smaller diameter. Proved by Lassak [La82], who showed more generally that \(2^{n-1} + 1\) parts suffice in \(\mathbb{R}^n\).

theorem borsuk_conjecture.four.nine_parts (s : Set (ℝ^4)) (hs : IsBounded s)
    (hs' : s.Nontrivial) : HasBorsukCover 9 s

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 155.

`Borsuk.borsuk_conjecture.four.eight_parts`

Solved: stated here without proof.

Partial result in dimension \(4\): every bounded subset of \(\mathbb{R}^4\) with at least two points can be partitioned into \(8\) sets of strictly smaller diameter. Claimed by Tolmachev and Voronov [TV26] via computer-assisted partitions of a truncated Lassak cover, with floating-point verification; the preprint is not yet refereed.

theorem borsuk_conjecture.four.eight_parts (s : Set (ℝ^4)) (hs : IsBounded s)
    (hs' : s.Nontrivial) : HasBorsukCover 8 s

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 166.

`Borsuk.borsuk_conjecture.one`

Textbook result, stated without proof. A Lean proof is at https://github.com/mo271/formal-conjectures/blob/07a6d25f07ba0e16a916be14e9830c36cfcb9777/FormalConjectures/Wikipedia/BorsukConjecture.lean#L126.

Borsuk's conjecture in dimension \(1\): a bounded set of reals with at least two points splits at the midpoint of its smallest enclosing interval into two parts of smaller diameter.

theorem borsuk_conjecture.one : BorsukConjecture 1

Category textbook; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 184.

`Borsuk.borsuk_conjecture.two`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/07a6d25f07ba0e16a916be14e9830c36cfcb9777/FormalConjectures/Wikipedia/BorsukConjecture.lean#L131.

Borsuk's conjecture in the plane, proved by Borsuk [Bo33].

theorem borsuk_conjecture.two : BorsukConjecture 2

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 192.

`Borsuk.borsuk_conjecture.three`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/07a6d25f07ba0e16a916be14e9830c36cfcb9777/FormalConjectures/Wikipedia/BorsukConjecture.lean#L136.

Borsuk's conjecture in dimension \(3\), proved by Perkal [Pe47] and Eggleston [Eg55].

theorem borsuk_conjecture.three : BorsukConjecture 3

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 200.

`Borsuk.borsuk_conjecture.not_forall`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/07a6d25f07ba0e16a916be14e9830c36cfcb9777/FormalConjectures/Wikipedia/BorsukConjecture.lean#L144.

Borsuk's conjecture is false in general: Kahn and Kalai [KK93] gave counterexamples in dimension \(1325\) and in every dimension \(n > 2014\).

theorem borsuk_conjecture.not_forall : ¬ ∀ n, BorsukConjecture n

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 211.

`Borsuk.borsuk_conjecture.not_sixty_five`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/07a6d25f07ba0e16a916be14e9830c36cfcb9777/FormalConjectures/Wikipedia/BorsukConjecture.lean#L149.

Borsuk's conjecture fails in dimension \(65\), by Bondarenko [Bo14].

theorem borsuk_conjecture.not_sixty_five : ¬ BorsukConjecture 65

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 219.

`Borsuk.borsuk_conjecture.not_sixty_four`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/07a6d25f07ba0e16a916be14e9830c36cfcb9777/FormalConjectures/Wikipedia/BorsukConjecture.lean#L157.

Borsuk's conjecture fails in dimension \(64\), by Jenrich and Brouwer [JB14]. This is the smallest dimension with a refereed counterexample.

theorem borsuk_conjecture.not_sixty_four : ¬ BorsukConjecture 64

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 230.

`Borsuk.borsuk_conjecture.not_sixty_three`

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/07a6d25f07ba0e16a916be14e9830c36cfcb9777/FormalConjectures/Wikipedia/BorsukConjecture.lean#L166.

Borsuk's conjecture fails in dimension \(63\), by a 321-point configuration found in 2026 by Grinsztajn [Gr26] and independently by Konz and Ji [Ji26]. This was the smallest dimension with a known counterexample before [OAI26].

theorem borsuk_conjecture.not_sixty_three : ¬ BorsukConjecture 63

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 242.

`Borsuk.borsuk_conjecture.not_nine`

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Geometry/Borsuk/Main.lean#L117.

Borsuk's conjecture fails in dimension \(9\): the set of rank-one orthogonal projectors on \(\mathbb{R}^4\), a compact subset of the nine-dimensional Euclidean space of trace-one symmetric \(4 \times 4\) matrices with the Frobenius metric, has diameter \(\sqrt{2}\) and cannot be covered by \(10\) sets of smaller diameter. This was proved by an internal OpenAI model in September 2026 [OAI26]; see the linked Lean proof. This is the smallest dimension in which the conjecture is currently known to be false.

theorem borsuk_conjecture.not_nine : ¬ BorsukConjecture 9

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 256.

`Borsuk.borsuk_conjecture.not_of_nine_le`

Solved: stated here without proof.

Borsuk's conjecture fails in every dimension \(n \geq 9\). Corollary 7.1 of [OAI26] extends the dimension-nine counterexample by adjoining \(n - 9\) points at diameter distance from one another and from the original set.

theorem borsuk_conjecture.not_of_nine_le (n : ℕ) (hn : 9 ≤ n) : ¬ BorsukConjecture n

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/BorsukConjecture.lean, line 263.

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

*abc* conjecture to Borsuk's conjecture

Theorem*abc* conjecture#

ABC.abc

ABC.abc.variants.lt_constant_mul

ABC.abc.variants.quality

Sources

TheoremAgoh-Giuga conjecture#

AgohGiuga.agoh_giuga

AgohGiuga.agoh_giuga.variants.giuga

AgohGiuga.agoh_giuga.variants.equivalence

AgohGiuga.isWeakGiuga_iff_prime_dvd

AgohGiuga.isWeakGiuga_iff_sum_primeFactors

AgohGiuga.squarefree_of_isCarmichael

AgohGiuga.korselts_criterion

AgohGiuga.isStrongGiuga_iff

AgohGiuga.agoh_giuga.variants.isStrongGiuga_implies_isCarmichael

AgohGiuga.agoh_giuga.variants.le_primeFactors_card_of_isStrongGiuga

AgohGiuga.agoh_giuga.variants._1000_le_digits_length_of_isStrongGiuga

AgohGiuga.agoh_giuga.variants._1700_le_digits_length_of_isStrongGiuga

AgohGiuga.agoh_giuga.variants._13000_le_digits_length_of_isStrongGiuga

AgohGiuga.agoh_giuga.variants.isStrongGiuga_growth

Sources

TheoremAgrawal's conjecture#

AgrawalConjecture.agrawal_conjecture

AgrawalConjecture.agrawal_conjecture.variants.popovych

Sources

TheoremNormality of Irrational Algebraic Numbers#

AlgebraicNormality.irrational_algebraic_absolutely_normal

AlgebraicNormality.irrational_algebraic_normal_in_some_base

Sources

TheoremNon-Power-of-2 Almost Perfect Numbers Conjecture#

AlmostPerfectNumbers.exists_almost_perfect_not_power_of_two

Sources

TheoremThe Alon–Saks–Seymour conjecture (disproved)#

AlonSaksSeymourConjecture.alon_saks_seymour_conjecture

AlonSaksSeymourConjecture.alon_saks_seymour_conjecture.variants.graham_pollak

AlonSaksSeymourConjecture.alon_saks_seymour_conjecture.variants.huang_sudakov

Sources

TheoremAlspach's conjecture on cycle decompositions of complete graphs (1981; proved 2014)#

AlspachConjecture.alspach_conjecture

AlspachConjecture.alspach_conjecture.variants.even

AlspachConjecture.alspach_conjecture.variants.long_cycles

AlspachConjecture.alspach_conjecture.variants.oberwolfach

Sources

TheoremAmicable numbers#

AmicableNumbers.relatively_prime_amicable

AmicableNumbers.infinitely_many_amicable

AmicableNumbers.opposite_parity_amicable

Sources

TheoremThe Andrews-Curtis conjecture#

AndrewsCurtis.andrews_curtis_conjecture

Sources

TheoremAndrica's conjecture#

Andrica.andrica_conjecture

Andrica.andrica_conjecture.ferreira_large_n

Sources

TheoremArtin's conjecture on primitive roots#

ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.i

ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.i

ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.ii

ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.ii

ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_square_or_minus_one

ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one

ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one

ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one

ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one

Sources

TheoremBalanced prime conjecture#

BalancedPrimes.balanced_primes

BalancedPrimes.balanced_primes_order

Sources

TheoremBateman-Horn Conjecture#

BatemanHornConjecture.bateman_horn_conjecture

Sources

TheoremBeal conjecture#

BealConjecture.beal_conjecture

BealConjecture.flt_of_beal_conjecture

Sources

TheoremBeck–Fiala theorem and conjecture#

BeckFiala.beck_fiala_theorem

abc conjecture to Borsuk's conjecture

Theoremabc conjecture #

`ABC.abc`

`ABC.abc.variants.lt_constant_mul`

`ABC.abc.variants.quality`

TheoremAgoh-Giuga conjecture #

`AgohGiuga.agoh_giuga`

`AgohGiuga.agoh_giuga.variants.giuga`

`AgohGiuga.agoh_giuga.variants.equivalence`

`AgohGiuga.isWeakGiuga_iff_prime_dvd`

`AgohGiuga.isWeakGiuga_iff_sum_primeFactors`

`AgohGiuga.squarefree_of_isCarmichael`

`AgohGiuga.korselts_criterion`

`AgohGiuga.isStrongGiuga_iff`

`AgohGiuga.agoh_giuga.variants.isStrongGiuga_implies_isCarmichael`

`AgohGiuga.agoh_giuga.variants.le_primeFactors_card_of_isStrongGiuga`

`AgohGiuga.agoh_giuga.variants._1000_le_digits_length_of_isStrongGiuga`

`AgohGiuga.agoh_giuga.variants._1700_le_digits_length_of_isStrongGiuga`

`AgohGiuga.agoh_giuga.variants._13000_le_digits_length_of_isStrongGiuga`

`AgohGiuga.agoh_giuga.variants.isStrongGiuga_growth`

TheoremAgrawal's conjecture #

`AgrawalConjecture.agrawal_conjecture`

`AgrawalConjecture.agrawal_conjecture.variants.popovych`

TheoremNormality of Irrational Algebraic Numbers #

`AlgebraicNormality.irrational_algebraic_absolutely_normal`

`AlgebraicNormality.irrational_algebraic_normal_in_some_base`

TheoremNon-Power-of-2 Almost Perfect Numbers Conjecture #

`AlmostPerfectNumbers.exists_almost_perfect_not_power_of_two`

`AlonSaksSeymourConjecture.alon_saks_seymour_conjecture`

`AlonSaksSeymourConjecture.alon_saks_seymour_conjecture.variants.graham_pollak`

`AlonSaksSeymourConjecture.alon_saks_seymour_conjecture.variants.huang_sudakov`

`AlspachConjecture.alspach_conjecture`

`AlspachConjecture.alspach_conjecture.variants.even`

`AlspachConjecture.alspach_conjecture.variants.long_cycles`

`AlspachConjecture.alspach_conjecture.variants.oberwolfach`

TheoremAmicable numbers #

`AmicableNumbers.relatively_prime_amicable`

`AmicableNumbers.infinitely_many_amicable`

`AmicableNumbers.opposite_parity_amicable`

TheoremThe Andrews-Curtis conjecture #

`AndrewsCurtis.andrews_curtis_conjecture`

TheoremAndrica's conjecture #

`Andrica.andrica_conjecture`

`Andrica.andrica_conjecture.ferreira_large_n`

TheoremArtin's conjecture on primitive roots #

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.i`

`ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.i`

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.ii`

`ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.parts.ii`

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_square_or_minus_one`

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one`

`ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one`

`ArtinPrimitiveRootsConjecture.artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one`

`ArtinPrimitiveRootsConjecture.conditional_artin_primitive_roots.variants.part_ii_power_squarefreePart_modeq_one`

TheoremBalanced prime conjecture #

`BalancedPrimes.balanced_primes`

`BalancedPrimes.balanced_primes_order`

TheoremBateman-Horn Conjecture #

`BatemanHornConjecture.bateman_horn_conjecture`

TheoremBeal conjecture #

`BealConjecture.beal_conjecture`

`BealConjecture.flt_of_beal_conjecture`

TheoremBeck–Fiala theorem and conjecture #

`BeckFiala.beck_fiala_theorem`

`BeckFiala.beck_fiala_conjecture`

TheoremThe Berge–Fulkerson conjecture #

`BergeFulkersonConjecture.berge_fulkerson_conjecture`

`BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.berge`

`BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.fan_raspaud`

`BergeFulkersonConjecture.berge_fulkerson_conjecture.variants.petersen`

TheoremBetrothed numbers #

`BetrothedNumbers.same_parity_betrothed`

`BetrothedNumbers.infinitely_many_betrothed`

TheoremThe Bing-Borsuk Conjecture #

`BingBorsuk.bing_borsuk_conjecture`

TheoremBloch and Landau constants #

`Bloch.blochConstant_lower_bound`

`Bloch.blochConstant_upper_bound`

`Bloch.blochConstant_exact_value`

`Bloch.univalentBlochConstant_lower_bound`