Gauss circle problem to Inverse Galois problem

TheoremGauss circle problem#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/GaussCircleProblem.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.

GaussCircleProblem.error_le

Solved: stated here without proof.

Gauss proved that

\[ |E(r)|\leq 2\sqrt{2}\pi r, \]

for sufficiently large \(r\).

[Ha59] Hardy, G. H. (1959). Ramanujan: Twelve Lectures on Subjects Suggested by His Life and Work(3rd ed.). New York: Chelsea Publishing Company. p. 67

theorem error_le : ∀ᶠ r in atTop, |E r| ≤ 2 * √2 * π * r

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

GaussCircleProblem.error_not_isLittleO

Solved: stated here without proof.

Hardy and Laundau independently found a lower bound by showing that

\[ |E(r)| \neq o\left(r^{1/2}(\log r)^{1/4}\right) \]
theorem error_not_isLittleO : ¬E =o[atTop] (fun r => √r * √√r.log)

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

GaussCircleProblem.error_isBigO

Open: stated without proof.

It is conjectured that the correct bound is

\[ |E(r)| = O\left(r^{1/2 + o(1)}\right) \]

[Ha59] Hardy, G. H. (1959). Ramanujan: Twelve Lectures on Subjects Suggested by His Life and Work(3rd ed.). New York: Chelsea Publishing Company. p. 67

See also https://arxiv.org/abs/2305.03549

theorem error_isBigO : ∃ (o : ℝ → ℝ) (_ : Tendsto o atTop (𝓝 0)),
    E =O[atTop] fun r => r ^ (1/2 + o r)

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

GaussCircleProblem.exact_form_floor

Solved: stated here without proof.

The value of \(N(r)\) can be expressed as

\[ N(r) = 1 + 4\sum_{i=0}^{\infty}\left(\left\lfloor\frac{r^2}{4i+1}\right\rfloor - \left\lfloor\frac{r^2}{4i + 3}\right\rfloor\right). \]
theorem exact_form_floor (r : ℝ) (hr : 0 ≤ r) :
    N r = 1 + 4 * ∑' (i : ℕ), (⌊r ^ 2 / (4 * i + 1)⌋ - ⌊r ^ 2 / (4 * i + 3)⌋)

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

Sources
LeanGaussCircleProblem.error_le · GaussCircleProblem.error_not_isLittleO · GaussCircleProblem.error_isBigO · GaussCircleProblem.exact_form_floor

TheoremGilbreath's conjecture#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/Gilbreath.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.

Gilbreath.gilbreath_conjecture

Open: stated without proof.

Gilbreath's conjecture Gilbreath's conjecture states that every term in the sequence \(d^k_0\) for \(k > 0\) is equal to 1.

theorem gilbreath_conjecture (k : ℕ+) : d k 0 = 1

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

Sources
LeanGilbreath.gilbreath_conjecture

TheoremGoldbach's conjecture#

References: - Landau Problems Wikipedia Page - Goldbach's Conjecture Wikipedia Page

Quoted from FormalConjectures/Wikipedia/GoldbachConjecture.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.

GoldbachConjecture.goldbach

Open: stated without proof.

Can every even integer greater than 2 be written as the sum of two primes?

theorem goldbach :
    ∀ n : ℕ, 2 < n → Even n → ∃ p q, Prime p ∧ Prime q ∧ n = p + q

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

TernaryGoldbachConjecture.ternaryGoldbach

Solved: stated here without proof.

Can every odd integer greater than 5 be written as the sum of three primes? (A prime may be used more than once.)

NB. While Harald Helfgott's solution is not published in a peer-reviewed journal yet, his results seem generally accepted.

theorem ternaryGoldbach (n : ℕ) (hn : 5 < n) (hn_odd : Odd n) :
    ∃ p q r, Nat.Prime p ∧ Nat.Prime q ∧ Nat.Prime r ∧ n = p + q + r

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

Sources
LeanGoldbachConjecture.goldbach · TernaryGoldbachConjecture.ternaryGoldbach

TheoremGoodman's conjecture on coefficients of \(p\)-valent functions#

A regular (analytic) function is \(p\)-valent on the unit disk if it assumes each value at most \(p\) times there, and some value exactly \(p\) times. For such a function \(f(z) = \sum_{n \ge 1} b_n z^n\) (so \(f(0) = 0\)), Goodman's conjecture (1948) asserts that its coefficients satisfy

\[|b_n| \le \sum_{k=1}^{p} \frac{2k (n+p)!}{(p-k)!\,(p+k)!\,(n-p-1)!\,(n^2-k^2)} |b_k| \qquad (n > p).\]

This generalises the classical coefficient bounds for univalent functions (the case \(p = 1\), where the bound reads \(|b_n| \le n\,|b_1|\), i.e. \(|b_n| \le n\) under the classical normalisation \(b_1 = 1\)) to \(p\)-valent functions. It has been verified in several special cases, including \(p\)-valent typically-real functions.

References: - Wikipedia - Goodman, A. W., On some determinants related to \(p\)-valent functions, Trans. Amer. Math. Soc. 63 (1948), 175–192.

Quoted from FormalConjectures/Wikipedia/GoodmanConjecture.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. It also has 2 test statements, counted here but not shown.

GoodmanConjecture.goodman_conjecture

Open: stated without proof.

Goodman's conjecture. For every \(p\)-valent normalised function \(f\) on the unit disk and every \(n > p\), the \(n\)-th coefficient is bounded by the Goodman bound:

\[|b_n| \le \sum_{k=1}^{p} \frac{2k (n+p)!}{(p-k)!\,(p+k)!\,(n-p-1)!\,(n^2-k^2)} |b_k|.\]
theorem goodman_conjecture (f : ℂ → ℂ) (p n : ℕ) (hf : IsPValent f p)
    (hf' : IsNormalized f) (hn : p < n) :
    ‖coeff f n‖ ≤ goodmanBound f p n

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

Sources
LeanGoodmanConjecture.goodman_conjecture

TheoremThe Goormaghtigh conjecture#

A repunit is a number whose digits in some base are all \(1\). Here a nontrivial representation has at least three digits. The Goormaghtigh conjecture says that \(31\) and \(8191\) are the only numbers having nontrivial repunit representations in two different bases.

References: * Wikipedia * J. Grantham, No new Goormaghtigh primes up to \(10^{700}\)

Quoted from FormalConjectures/Wikipedia/Goormaghtigh.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. It also has 3 test statements, counted here but not shown.

Goormaghtigh.goormaghtigh_conjecture

Open: stated without proof.

The only Goormaghtigh numbers are \(31\) and \(8191\).

theorem goormaghtigh_conjecture (N : ℕ) (hN : IsGoormaghtighNumber N) :
    N = 31 ∨ N = 8191

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

Sources
LeanGoormaghtigh.goormaghtigh_conjecture

TheoremGraceful Tree Conjecture (Ringel–Kotzig conjecture)#

Reference: Wikipedia/Graceful_labeling

Conjectured by Ringel (1963) and Kotzig; formalized by Rosa (1967).

Quoted from FormalConjectures/Wikipedia/GracefulLabeling.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. It also has 2 test statements, counted here but not shown.

GracefulLabeling.graceful_tree_conjecture

Open: stated without proof.

Every tree admits a graceful labeling.

A graceful labeling of a tree \(T\) with \(m\) edges is an injective map \(f : V \to \{0, \dots, m\}\) such that the multiset of absolute differences \(|f(u) - f(v)|\) over edges \(\{u,v\}\) of \(T\) equals \(\{1, \dots, m\}\).

theorem graceful_tree_conjecture {V : Type*} [Fintype V] [DecidableEq V]
    (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree) :
    let m := T.edgeFinset.card
    ∃ f : V → ℕ,
      Function.Injective f ∧
      (∀ v, f v ≤ m) ∧
      T.edgeFinset.image (fun e =>
        e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)),
                fun u v => by
                  show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbs
                  rw [← Int.natAbs_neg, neg_sub]⟩) = Finset.Icc 1 m

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

Sources
LeanGracefulLabeling.graceful_tree_conjecture

TheoremGrimm's conjecture#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/Grimm.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.

Grimm.grimm_conjecture

Open: stated without proof.

Grimm's Conjecture If \(n, n+1, \dots, n+k-1\) are all composite numbers, then there are \(k\) distinct primes \(p_i\) such that \(p_i\) divides \(n + i\) for all \(0 \le i \le k-1\).

theorem grimm_conjecture (n k : ℕ) (hn : 1 ≤ n) (hk : 1 ≤ k)
    (h : ∀ i : Fin k, (n + i).Composite) :
    ∃ ps : Fin k ↪ ℕ,  ∀ i : Fin k, (ps i).Prime ∧ ps i ∣ (n + i)

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

Grimm.grimm_conjecture_weak

Open: stated without proof.

Grimm's Conjecture, weaker version If \(n, n+1, \dots, n+k-1\) are all composite numbers, then their product has at least \(k\) distinct prime divisors.

theorem grimm_conjecture_weak (n k : ℕ) (hn : 1 ≤ n) (hk : 1 ≤ k)
    (h : ∀ i : Fin k, (n + i).Composite) :
    ∃ ps : Fin k ↪ ℕ,  ∀ i : Fin k, (ps i).Prime ∧ ∃ j : Fin k, ps i ∣ (n + j)

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

Sources
LeanGrimm.grimm_conjecture · Grimm.grimm_conjecture_weak

TheoremGromov's theorem on groups of polynomial growth#

Reference: - Wikipedia

Quoted from FormalConjectures/Wikipedia/GromovPolynomialGrowth.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 solved. It also has 1 test statement, counted here but not shown.

GromovPolynomialGrowth.GromovPolynomialGrowthTheorem

Solved: stated here without proof.

Gromov's Polynomial Growth Theorem : A finitely generated group has polynomial growth if and only if it is virtually nilpotent.

theorem GromovPolynomialGrowthTheorem [Group.FG G] :
    HasPolynomialGrowth G ↔ Group.IsVirtuallyNilpotent G

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/GromovPolynomialGrowth.lean, line 61.

Sources
LeanGromovPolynomialGrowth.GromovPolynomialGrowthTheorem

TheoremThe Gyárfás–Sumner conjecture#

References: * Wikipedia * [Gy75] Gyárfás, A. (1975). "On Ramsey covering-numbers." Infinite and finite sets, Colloq. Math. Soc. János Bolyai 10, pp. 801--816. * [Su81] Sumner, D. P. (1981). "Subtrees of a graph and the chromatic number." The theory and applications of graphs (Kalamazoo, 1980), Wiley, pp. 557--576. * [Gy87] Gyárfás, A. (1987). "Problems from the world surrounding perfect graphs." Zastos. Mat. 19, pp. 413--441. * [KP94] Kierstead, H. A. and Penrice, S. G. (1994). "Radius two trees specify χ-bounded classes." J. Graph Theory 18, pp. 119--129. * [SS20] Scott, A. and Seymour, P. (2020). "A survey of χ-boundedness." J. Graph Theory 95, pp. 473--504. arXiv:1812.07500

Quoted from FormalConjectures/Wikipedia/GyarfasSumnerConjecture.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: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.

GyarfasSumnerConjecture.gyarfas_sumner_conjecture

Open: stated without proof.

The Gyárfás–Sumner conjecture (Gyárfás 1975, Sumner 1981).

For every finite tree \(T\) the class of \(T\)-free graphs (graphs with no induced subgraph isomorphic to \(T\)) is \(\chi\)-bounded: there is a function \(f\) such that every \(T\)-free graph \(G\) satisfies \(\chi(G) \le f(\omega(G))\).

theorem gyarfas_sumner_conjecture :
    ∀ {W : Type} [Fintype W] [DecidableEq W] (T : SimpleGraph W) [DecidableRel T.Adj],
      T.IsTree → ∃ f : ℕ → ℕ, IsChiBoundedBy T f

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

GyarfasSumnerConjecture.gyarfas_sumner_conjecture.variants.path

Solved: stated here without proof.

Paths (Gyárfás 1987).

For every \(n\), the class of \(P_n\)-free graphs is \(\chi\)-bounded. For \(n \ge 2\) and nonempty \(G\), Gyárfás's argument gives \(\chi(G) \le (n-1)^{\omega(G) - 1}\).

Reference: [Gy87].

theorem gyarfas_sumner_conjecture.variants.path (n : ℕ) :
    ∃ f : ℕ → ℕ, IsChiBoundedBy (pathGraph n) f

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

GyarfasSumnerConjecture.gyarfas_sumner_conjecture.variants.radius_two

Solved: stated here without proof.

Trees of radius two (Kierstead–Penrice 1994).

Every tree of radius at most \(2\) (i.e. with a vertex within distance \(2\) of every other vertex) specifies a \(\chi\)-bounded class.

Reference: [KP94].

theorem gyarfas_sumner_conjecture.variants.radius_two
    {W : Type} [Fintype W] [DecidableEq W] (T : SimpleGraph W) [DecidableRel T.Adj]
    (hT : T.IsTree) (hrad : ∃ c : W, ∀ w : W, T.dist c w ≤ 2) :
    ∃ f : ℕ → ℕ, IsChiBoundedBy T f

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

Sources
LeanGyarfasSumnerConjecture.gyarfas_sumner_conjecture · GyarfasSumnerConjecture.gyarfas_sumner_conjecture.variants.path · GyarfasSumnerConjecture.gyarfas_sumner_conjecture.variants.radius_two

TheoremHadamard's conjecture#

References: - Wikipedia - Tao's optimization constant 23a - Résolution d'une question relative aux déterminants by Jacques Hadamard, Bull. des sciences math., p.245, 1893

Quoted from FormalConjectures/Wikipedia/Hadamard.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: 2 open and 1 solved. It also has 3 test statements, counted here but not shown.

Hadamard.HadamardConjecture

Open: stated without proof.

There exists a Hadamard matrix for all \(n = 4k\).

theorem HadamardConjecture (k : ℕ) : ∃ M, IsHadamard (n := 4 * k) M

Category research open; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Wikipedia/Hadamard.lean, line 91.

Hadamard.HadamardConjecture.variants.first_cases

Solved: stated here without proof.

For all \(k ≤ 166\), it is known there that there is a Hadamard matrix of size \(4 * k\). So hadamardConstant is at least \(668\).

theorem HadamardConjecture.variants.first_cases : 668 ≤ hadamardConstant

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Wikipedia/Hadamard.lean, line 142.

Hadamard.HadamardConjecture.variants.«167»

Open: stated without proof.

The smallest order for which no Hadamard matrix is presently known is \(668 = 4 * 167\). Is hadamardConstant larger than \(668\)?

theorem HadamardConjecture.variants.«167» : 668 < hadamardConstant

Category research open; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Wikipedia/Hadamard.lean, line 150.

Sources
LeanHadamard.HadamardConjecture · Hadamard.HadamardConjecture.variants.first_cases · Hadamard.HadamardConjecture.variants.«167»

TheoremHajós' conjecture (1961) — disproved#

References: * Wikipedia * [Ha61] Hajós, G. (1961). "Über eine Konstruktion nicht n-färbbarer Graphen." Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe 10, pp. 116--117. * [Di52] Dirac, G. A. (1952). "A property of 4-chromatic graphs and some remarks on critical graphs." J. London Math. Soc. 27, pp. 85--92. * [Ca79] Catlin, P. A. (1979). "Hajós' graph-coloring conjecture: variations and counterexamples." J. Combin. Theory Ser. B 26, pp. 268--274. * [EF81] Erdős, P. and Fajtlowicz, S. (1981). "On the conjecture of Hajós." Combinatorica 1, pp. 141--143. * [Th05] Thomassen, C. (2005). "Some remarks on Hajós' conjecture." J. Combin. Theory Ser. B 93, pp. 95--105.

Quoted from FormalConjectures/Wikipedia/HajosConjecture.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 1 API statement, counted here but not shown.

HajosConjecture.hajos_conjecture

Solved: stated here without proof.

Hajós' conjecture (1961) — disproved.

Hajós conjectured that every graph with chromatic number at least \(k\) contains a subdivision of \(K_k\) (a strengthening of Hadwiger's conjecture). This is false: Catlin [Ca79] gave counterexamples for every \(k \ge 7\), and Erdős and Fajtlowicz [EF81] showed that almost all graphs are counterexamples.

theorem hajos_conjecture : ¬
    ∀ {V : Type} [Fintype V] (G : SimpleGraph V) (k : ℕ),
      (k : ℕ∞) ≤ G.chromaticNumber → ContainsSubdivision (completeGraph (Fin k)) G

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

HajosConjecture.hajos_conjecture.variants.le_four

Solved: stated here without proof.

The cases \(k \le 4\) (Dirac 1952).

Every graph with chromatic number at least \(4\) contains a subdivision of \(K_4\); the cases \(k \le 3\) are elementary.

Reference: [Di52].

theorem hajos_conjecture.variants.le_four
    {V : Type} [Fintype V] (G : SimpleGraph V) (k : ℕ) (hk : k ≤ 4)
    (h : (k : ℕ∞) ≤ G.chromaticNumber) : ContainsSubdivision (completeGraph (Fin k)) G

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

HajosConjecture.hajos_conjecture.variants.five_six

Open: stated without proof.

The cases \(k = 5\) and \(k = 6\) remain open.

Whether every \(5\)-chromatic graph contains a subdivision of \(K_5\), and every \(6\)-chromatic graph a subdivision of \(K_6\), is unknown (see [Th05]).

theorem hajos_conjecture.variants.five_six :
    ∀ {V : Type} [Fintype V] (G : SimpleGraph V) (k : ℕ), k = 5 ∨ k = 6 →
      (k : ℕ∞) ≤ G.chromaticNumber → ContainsSubdivision (completeGraph (Fin k)) G

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

HajosConjecture.hajos_conjecture.variants.catlin

Solved: stated here without proof.

Catlin (1979): counterexamples for every \(k \ge 7\).

Reference: [Ca79].

theorem hajos_conjecture.variants.catlin (k : ℕ) (hk : 7 ≤ k) :
    ∃ (V : Type) (_ : Fintype V) (G : SimpleGraph V),
      (k : ℕ∞) ≤ G.chromaticNumber ∧ ¬ ContainsSubdivision (completeGraph (Fin k)) G

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

Sources
LeanHajosConjecture.hajos_conjecture · HajosConjecture.hajos_conjecture.variants.le_four · HajosConjecture.hajos_conjecture.variants.five_six · HajosConjecture.hajos_conjecture.variants.catlin

TheoremHall's conjecture#

There exists a positive number \(C\) such that for any integer \(x, y\) with \(y^2 \ne x^3\), \(|y^2 - x^3| > C \sqrt{|x|}\).

References: - Wikipedia - L. Danilov, The Diophantine equation \(x^3 - y^2 = k\) and Hall's conjecture, Mathematical notes of the Academy of Sciences of the USSR 32 (1982): 617-618

Quoted from FormalConjectures/Wikipedia/Hall.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: 2 open and 1 solved. It also has 1 test statement, counted here but not shown.

Hall.hall_conjecture

Open: stated without proof.

Original Hall's conjecture with exponent \(1/2\).

theorem hall_conjecture : HallConjectureExp 2⁻¹

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

Hall.danilov

Solved: stated here without proof.

Danilov proved that one cannot replace the exponent \(1/2\) with larger number. In other words, for any \(\delta > 0\), there is no positive constant \(C\) such that \(|y^2 - x^3| > C |x| ^ {1/2 + \delta}\) for all integers \(x, y\) with \(y^2 \ne x^3\).

theorem danilov (δ : ℝ) (h : δ > 0) : ¬ HallConjectureExp (2⁻¹ + δ)

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

Hall.weak_hall_conjecture

Open: stated without proof.

Weak form of Hall's conjecture: relax the exponent from \(1/2\) to \(1/2 - \varepsilon\).

theorem weak_hall_conjecture (ε : ℝ) (hε : ε > 0) : HallConjectureExp (2⁻¹ - ε)

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

Sources
LeanHall.hall_conjecture · Hall.danilov · Hall.weak_hall_conjecture

TheoremFirst Hardy–Littlewood conjecture#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/HardyLittlewood.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: 2 open and 1 solved.

HardyLittlewood.first_hardy_littlewood_conjecture

Open: stated without proof.

Let \(P = (m_1, \dots, m_k)\) be a tuple of distinct positive even integers. Let \(\pi_P(n)\) denote the number of primes \(p\leq n\) such that \((p, p + m_1, \dots, p + m_k)\) forms an admissible prime constellation. Let \(w(q; m_1, \dots, m_k)\) denote the number of distinct residues of \(0, m_1, \dots, m_k\) modulo \(q\), and let

\[ C_P = 2 ^ k\prod_{\substack{q\ \text{prime} \\ q\geq 3}} \frac{1 - \frac{w(q; m_1, \dots, m_k)}{q}}{\left(1 - \frac{1}{q}\right)^{k+1}}. \]

Then

\[ \pi_P(n)\sim C_P\int_2^n\frac{dt}{\log^{k+1}t}. \]
theorem first_hardy_littlewood_conjecture {k : ℕ} (m : Fin k.succ → ℕ) :
    FirstHardyLittlewoodConjectureFor m

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

HardyLittlewood.second_hardy_littlewood_conjecture

Open: stated without proof.

For integers \(x, y \geq 2\),

\[ \pi(x + y) \leq \pi(x) + \pi(y), \]

where \(\pi(z)\) denotes the prime-counting function, giving the number of primes up to and including \(z\).

theorem second_hardy_littlewood_conjecture {x y : ℕ} (hx : 2 ≤ x) (hy : 2 ≤ y) :
    SecondHardyLittlewoodConjectureFor x y

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

HardyLittlewood.not_first_and_secondHardyLittlewoodConjecture

Solved: stated here without proof.

Richards [Ri74] showed that only one of the two Hardy-Littlewood conjectures can be true.

[Ri74] Richards, Ian (1974). On the Incompatibility of Two Conjectures Concerning Primes. Bull. Amer. Math. Soc. 80: 419–438.

theorem not_first_and_secondHardyLittlewoodConjecture :
    (∀ {k : ℕ} (m : Fin k.succ → ℕ), FirstHardyLittlewoodConjectureFor m) →
      ¬(∀ {x y : ℕ} (hx : 2 ≤ x) (hy : 2 ≤ y), SecondHardyLittlewoodConjectureFor x y)

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

Sources
LeanHardyLittlewood.first_hardy_littlewood_conjecture · HardyLittlewood.second_hardy_littlewood_conjecture · HardyLittlewood.not_first_and_secondHardyLittlewoodConjecture

TheoremThe Hasse--Weil conjecture for elliptic curves#

The \(L\)-series \(L(E, s)\) of an elliptic curve \(E\) over a number field converges absolutely on \(\operatorname{Re} s > 3/2\) ([Tate1966], p. 416; [Gross2011], Lecture 2, §1). The Hasse--Weil conjecture predicts that it has an analytic continuation to the whole complex plane and satisfies a functional equation ([Tate1966], p. 416; [Gross2011], Conjecture 2.7, stated there for the completed \(L\)-function). Only the continuation is stated here. Over \(\mathbb{Q}\) it follows from the modularity theorem.

[Wikipedia] states the conjecture for the Hasse--Weil zeta function and asks only for a meromorphic continuation, which is equivalent to a meromorphic continuation of \(L(E, s)\). That weaker form is the one the Birch and Swinnerton-Dyer conjecture rests on, so it is recorded here as well. [Gross2011], Conjecture 2.10 takes it as a hypothesis, and only near \(s = 1\). The formulation of the Birch and Swinnerton-Dyer conjecture in FormalConjectures/Millennium/BSD.lean instead asserts a global meromorphic continuation, so it implies exists_hasMeromorphicContinuation below.

References: - Wikipedia - [Tate1966] John Tate. "On the conjectures of Birch and Swinnerton-Dyer and a geometric analog." Seminaire Bourbaki, Vol. 9, Exp. No. 306 (1966), 415-440, numdam - [Gross2011] Benedict H. Gross. "Lectures on the conjecture of Birch and Swinnerton-Dyer." Arithmetic of L-functions, IAS/Park City Math. Ser. 18, AMS (2011), 169-209, math.harvard.edu

Quoted from FormalConjectures/Wikipedia/HasseWeil.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: 2 open and 1 solved. It also has 2 API statements, counted here but not shown.

HasseWeil.exists_hasMeromorphicContinuation

Open: stated without proof.

The \(L\)-series of an elliptic curve over a number field has a meromorphic continuation to \(\mathbb{C}\). This is the Hasse--Weil conjecture in the form stated in [Wikipedia], and a weak form of [Gross2011], Conjecture 2.7. It is also what the Birch and Swinnerton-Dyer conjecture rests on, as the hypothesis of [Gross2011], Conjecture 2.10.

theorem exists_hasMeromorphicContinuation (E : WeierstrassCurve K) [E.IsElliptic] :
    ∃ L, HasMeromorphicContinuation E L

Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/HasseWeil.lean, line 95.

HasseWeil.exists_hasAnalyticContinuation

Open: stated without proof.

The Hasse--Weil conjecture ([Tate1966], p. 416; [Gross2011], Conjecture 2.7): the \(L\)-series of an elliptic curve over a number field has an analytic continuation to \(\mathbb{C}\).

theorem exists_hasAnalyticContinuation (E : WeierstrassCurve K) [E.IsElliptic] :
    ∃ L, HasAnalyticContinuation E L

Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/HasseWeil.lean, line 103.

HasseWeil.exists_hasAnalyticContinuation_rat

Solved: stated here without proof.

The Hasse--Weil conjecture over \(\mathbb{Q}\): the \(L\)-series of an elliptic curve over \(\mathbb{Q}\) has an analytic continuation to \(\mathbb{C}\). This follows from the modularity theorem, see [Wikipedia].

theorem exists_hasAnalyticContinuation_rat (E : WeierstrassCurve ℚ) [E.IsElliptic] :
    ∃ L, HasAnalyticContinuation E L

Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/HasseWeil.lean, line 113.

Sources
LeanHasseWeil.exists_hasMeromorphicContinuation · HasseWeil.exists_hasAnalyticContinuation · HasseWeil.exists_hasAnalyticContinuation_rat

TheoremHedetniemi's conjecture (1966)#

References: * Wikipedia * [He66] Hedetniemi, S. T. (1966). Homomorphisms of graphs and automata. Technical Report 03105-44-T, University of Michigan. * [ES85] El-Zahar, M. and Sauer, N. (1985). "The chromatic number of the product of two 4-chromatic graphs is 4." Combinatorica 5, pp. 121--126. * [Sh19] Shitov, Y. (2019). "Counterexamples to Hedetniemi's conjecture." Ann. of Math. 190, pp. 663--667. arXiv:1905.02167 * [Ta22] Tardif, C. (2022). "The chromatic number of the product of 14-chromatic graphs can be 13." Combinatorica 42, pp. 301--308. * [Zh21] Zhu, X. (2021). "Relatively small counterexamples to Hedetniemi's conjecture." J. Combin. Theory Ser. B 146, pp. 141--150.

Quoted from FormalConjectures/Wikipedia/HedetniemiConjecture.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 API statement, counted here but not shown.

HedetniemiConjecture.hedetniemi_conjecture

Solved: stated here without proof.

Hedetniemi's conjecture (1966) — disproved.

For all finite simple graphs \(G\) and \(H\), the chromatic number of the tensor product was conjectured to satisfy \(\chi(G \times H) = \min\{\chi(G), \chi(H)\}\).

This is false: Shitov [Sh19] constructed finite graphs \(G\), \(H\) with \(\chi(G \times H) < \min\{\chi(G), \chi(H)\}\). The inequality \(\le\) always holds (chromaticNumber_tensorProd_le_min); it is the reverse inequality that fails.

theorem hedetniemi_conjecture : ¬
    ∀ {α β : Type} [Fintype α] [Fintype β] (G : SimpleGraph α) (H : SimpleGraph β),
      (tensorProd G H).chromaticNumber = min G.chromaticNumber H.chromaticNumber

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

HedetniemiConjecture.hedetniemi_conjecture.variants.el_zahar_sauer

Solved: stated here without proof.

El-Zahar–Sauer (1985): the conjecture holds when min {χ(G), χ(H)} ≤ 4.

If both \(G\) and \(H\) are \(4\)-chromatic then so is \(G \times H\); together with the easy cases \(\min\{\chi(G), \chi(H)\} \le 3\), this gives Hedetniemi's equality whenever \(\min\{\chi(G), \chi(H)\} \le 4\).

Reference: [ES85].

theorem hedetniemi_conjecture.variants.el_zahar_sauer
    {α β : Type} [Fintype α] [Fintype β] (G : SimpleGraph α) (H : SimpleGraph β)
    (h : min G.chromaticNumber H.chromaticNumber ≤ 4) :
    (tensorProd G H).chromaticNumber = min G.chromaticNumber H.chromaticNumber

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

HedetniemiConjecture.hedetniemi_conjecture.variants.shitov

Solved: stated here without proof.

Shitov (2019): the conjecture fails.

There exist finite graphs \(G\), \(H\) with \(\chi(G \times H) < \min\{\chi(G), \chi(H)\}\). Tardif [Ta22] later gave counterexamples with \(\min\{\chi(G),\chi(H)\} = 14\) and \(\chi(G \times H) = 13\), and Zhu [Zh21] considerably smaller ones.

References: [Sh19], [Ta22], [Zh21].

theorem hedetniemi_conjecture.variants.shitov :
    ∃ (α β : Type) (_ : Fintype α) (_ : Fintype β) (G : SimpleGraph α) (H : SimpleGraph β),
      (tensorProd G H).chromaticNumber < min G.chromaticNumber H.chromaticNumber

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

Sources
LeanHedetniemiConjecture.hedetniemi_conjecture · HedetniemiConjecture.hedetniemi_conjecture.variants.el_zahar_sauer · HedetniemiConjecture.hedetniemi_conjecture.variants.shitov

TheoremIdoneal numbers completeness conjecture#

An integer \(D>0\) is idoneal if every integer that can be expressed in exactly one way (up to order and signs) as \(x^2 + D y^2\) with gcd(x, Dy)=1 is a prime power or twice a prime power.

The Idoneal Numbers Completeness Conjecture asserts that the following list of 65 numbers is complete: 1,2,3,4,5,6,7,8,9,10,12,13,15,16,18,21,22,24,25,28,30,33,37,40,42,45,48, 57,58,60,70,72,78,85,88,93,102,105,112,120,130,133,165,168,177,190,210,232, 240,253,273,280,312,330,345,357,385,408,462,520,760,840,1320,1365,1848. References: - Wikipedia: Idoneal number - OEIS A000926

Quoted from FormalConjectures/Wikipedia/IdonealCompleteness.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. It also has 1 test statement, counted here but not shown.

Idoneal.idoneal_numbers_completeness

Open: stated without proof.

Idoneal numbers completeness conjecture.

theorem idoneal_numbers_completeness :
    ∀ n : ℕ, IsIdoneal n → n ∈ knownIdonealNumbers

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

Sources
LeanIdoneal.idoneal_numbers_completeness

TheoremInscribed square problem#

The inscribed square problem or Toeplitz conjecture asks whether every Jordan curve (i.e. simple close curve in ℝ²) admits an inscribed square, i.e. a square whose vertices all lie on the curve. There are several open and solved variants of this conjecture.

References: - Wikipedia - A Survey on the Square Peg Problem by Benjamin Matschke - arxiv/2005.09193

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

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

InscribedSquare.inscribed_square_problem

Open: stated without proof.

Inscribed square problem Does every Jordan curve admit an inscribed square?

theorem inscribed_square_problem :
    ∀ (γ : Circle → ℝ²) (hγ : IsEmbedding γ),
      ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1

Category research open; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/InscribedSquare.lean, line 57.

InscribedSquare.inscribed_rectangle_problem

Open: stated without proof.

Inscribed rectangle problem Does every Jordan curve admit inscribed rectangles of any given aspect ratio?

theorem inscribed_rectangle_problem :
    ∀ (γ : Circle → ℝ²) (hγ : IsEmbedding γ) (r : ℝ) (hr : r > 0),
      ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r

Category research open; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/InscribedSquare.lean, line 67.

InscribedSquare.exists_inscribed_rectangle

Solved: stated here without proof.

It is known that every Jordan curve admits at least one inscribed rectangle.

theorem exists_inscribed_rectangle (γ : Circle → ℝ²) (hγ : IsEmbedding γ) :
    ∃ t₁ t₂ t₃ t₄ r, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/InscribedSquare.lean, line 76.

InscribedSquare.exists_inscribed_rectangle_of_smooth

Solved: stated here without proof.

It is known that every smooth Jordan curve admits inscribed rectangles of all aspect ratios. Here a smooth Jordan curve is a smooth embedding of the circle into the plane, i.e. a smooth simple closed curve with nowhere vanishing velocity.

theorem exists_inscribed_rectangle_of_smooth (γ : Circle → ℝ²)
    (hγ : IsSmoothEmbedding (𝓡 1) (𝓡 2) ∞ γ) (r : ℝ) (hr : r > 0) :
    ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/InscribedSquare.lean, line 86.

InscribedSquare.exists_inscribed_square_of_C2

Solved: stated here without proof.

It is also known that every \(C^2\) Jordan curve admits an inscribed square. Here a \(C^2\) Jordan curve is a \(C^2\) embedding of the circle into the plane, i.e. a \(C^2\) simple closed curve with nowhere vanishing velocity.

theorem exists_inscribed_square_of_C2 (γ : Circle → ℝ²)
    (hγ : IsSmoothEmbedding (𝓡 1) (𝓡 2) 2 γ) :
    ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/InscribedSquare.lean, line 97.

Sources
LeanInscribedSquare.inscribed_square_problem · InscribedSquare.inscribed_rectangle_problem · InscribedSquare.exists_inscribed_rectangle · InscribedSquare.exists_inscribed_rectangle_of_smooth · InscribedSquare.exists_inscribed_square_of_C2

TheoremPolynomial-time computability of factoring#

This file formalizes the open problem of whether natural number / integer factorization can be computed in polynomial time on a deterministic classical Turing machine.

More precisely, it formalizes the following statement: Can the prime factorization of a natural number be computed in polynomial time (on a deterministic classical Turing machine)?

References: - Wikipedia: List of unsolved problems in computer science - Wikipedia: Integer factorization

Quoted from FormalConjectures/Wikipedia/IntegerFactorization.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.

PolyTime.isPolyTime_primeFactorsList

Open: stated without proof.

The integer factorization problem: Can the prime factorization of a positive integer be computed in polynomial time?

We state the problem by asking if Nat.primeFactorsList is polynomial-time computable (assuming typical encodings of ℕ and List ℕ into bitstrings).

Reference: Wikipedia

theorem isPolyTime_primeFactorsList : IsPolyTime Nat.primeFactorsList

Category research open; AMS 68 Computer science. Declared in FormalConjectures/Wikipedia/IntegerFactorization.lean, line 52.

Sources
LeanPolyTime.isPolyTime_primeFactorsList

TheoremInvariant Subspace Problem#

Reference: Wikipedia, Chalendar-Partington

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

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

InvariantSubspaceProblem.Invariant_subspace_problem

Open: stated without proof.

Show that every bounded linear operator T : H → H on a separable Hilbert space H of dimension at least 2 has a non-trivial closed T-invariant subspace: a closed linear subspace W of H, which is different from H and from {0}, such that T ( W ) ⊂ W. One needs the assumption that the dimension of H is at least 2 because otherwise any subspace would be either H or {0}.

theorem Invariant_subspace_problem [InnerProductSpace ℂ H] [TopologicalSpace.SeparableSpace H]
    [CompleteSpace H] (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) :
    Nonempty (ClosedInvariantSubspace T)

Category research open; AMS 47 Operator theory. Declared in FormalConjectures/Wikipedia/InvariantSubspaceProblem.lean, line 48.

InvariantSubspaceProblem.Invariant_subspace_problem_finite_dimensional

Proved here.

Every (bounded) linear operator T : H → H on a finite-dimensional normed space H of dimension at least 2 has a non-trivial (closed) T-invariant subspace. Since ℂ is algebraically closed, T has an eigenvector v ≠ 0, and the line ℂ ∙ v is such a subspace.

H is a complex normed space: with a bare Module ℂ H unrelated to the norm, finite-dimensional subspaces need not be closed, and the statement fails already in complex dimension 2.

theorem Invariant_subspace_problem_finite_dimensional [NormedSpace ℂ H] (h : FiniteDimensional ℂ H)
    (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) : Nonempty (ClosedInvariantSubspace T)

Category research solved; AMS 47 Operator theory. Declared in FormalConjectures/Wikipedia/InvariantSubspaceProblem.lean, line 61.

InvariantSubspaceProblem.Invariant_subspace_problem_non_separable

Proved here.

Every bounded linear operator T : H → H on a non-separable Hilbert space H has a non-trivial closed T-invariant subspace. Such an invariant space is given by considering the closure of the linear span of the orbit of any single non-zero vector.

theorem Invariant_subspace_problem_non_separable [InnerProductSpace ℂ H] [CompleteSpace H]
    (h : ¬TopologicalSpace.SeparableSpace H) (T : H →L[ℂ] H) :
    Nonempty (ClosedInvariantSubspace T)

Category research solved; AMS 47 Operator theory. Declared in FormalConjectures/Wikipedia/InvariantSubspaceProblem.lean, line 100.

InvariantSubspaceProblem.Invariant_subspace_problem_normal_operator

Solved: stated here; a Lean proof is at https://github.com/baobingzhang/jsp-000024-lomonosov-lean/blob/8b43adc9781d70deb3d23bcdf38ec6195683669b/InvariantSubspaceLomonosov.lean#L422-L424; a Lean proof is at https://github.com/zblore/fc-isp-normal/blob/399f8bd8b68d4e24f33a6077e01a4adf3ae51df6/ISPNormal/Normal.lean#L143-L144.

Every normal linear operator T : H → H on a Hilbert space H of dimension at least 2 has a non-trivial closed T-invariant subspace. If T is a multiple of the identity, one can take any non-trivial subspace. If not, one can take any nontrivial spectral subspace of T.

theorem Invariant_subspace_problem_normal_operator [InnerProductSpace ℂ H] [CompleteSpace H]
    (hdim : 2 ≤ Module.rank ℂ H) (T : H →L[ℂ] H) [IsStarNormal T]:
    Nonempty (ClosedInvariantSubspace T)

Category research solved; AMS 47 Operator theory. Declared in FormalConjectures/Wikipedia/InvariantSubspaceProblem.lean, line 138.

InvariantSubspaceProblem.Invariant_subspace_problem_l1

Solved: stated here; a Lean proof is at https://github.com/zblore/fc-read-l1/blob/57ceaa0ecdea86e90d82c1fd241c17e3bdb93e2d/ReadL1/Main.lean#L24-L27.

There exists a bounded linear operator T on the l1 space (lp (fun (_ : ℕ) => ℂ) 1)) without non-trivial closed T-invariant subspace Read 1985, see also the first counterexample by Enflo Enflo 1987, submitted in 1981.

theorem Invariant_subspace_problem_l1 :
    ∃ (T : (lp (fun (_ : ℕ) => ℂ) 1) →L[ℂ] (lp (fun (_ : ℕ) => ℂ) 1)),
    IsEmpty (ClosedInvariantSubspace T)

Category research solved; AMS 47 Operator theory. Declared in FormalConjectures/Wikipedia/InvariantSubspaceProblem.lean, line 151.

Sources
LeanInvariantSubspaceProblem.Invariant_subspace_problem · InvariantSubspaceProblem.Invariant_subspace_problem_finite_dimensional · InvariantSubspaceProblem.Invariant_subspace_problem_non_separable · InvariantSubspaceProblem.Invariant_subspace_problem_normal_operator · InvariantSubspaceProblem.Invariant_subspace_problem_l1

TheoremInverse Galois problem#

Reference: Wikipedia

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

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

InverseGalois.inverse_galois_problem

Open: stated without proof.

The Inverse Galois Problem: every finite group is isomorphic to the Galois group of a Galois extension of the rationals.

theorem inverse_galois_problem {G : Type*} [Fintype G] [Group G] :
    IsRealizable ℚ G

Category research open; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/InverseGalois.lean, line 53.

InverseGalois.inverse_galois_problem.variants.cyclic

Solved: stated here without proof.

Every finite cyclic group is realizable.

theorem inverse_galois_problem.variants.cyclic
    {G : Type*} [Fintype G] [Group G] [IsCyclic G] :
    IsRealizable ℚ G

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/InverseGalois.lean, line 61.

InverseGalois.inverse_galois_problem.variants.abelian

Solved: stated here without proof.

Every finite abelian group is realizable.

theorem inverse_galois_problem.variants.abelian
    {G : Type*} [Fintype G] [CommGroup G] :
    IsRealizable ℚ G

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/InverseGalois.lean, line 70.

InverseGalois.inverse_galois_problem.variants.symmetric_group

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/4e37e8779287010f34ffc6c817ea45fc26d8ba0a/Proofs/T_InverseGalois_inverse_galois_problem_variants_symmetric_group.lean#L392.

Every finite symmetric group is realizable.

theorem inverse_galois_problem.variants.symmetric_group
    {S : Type*} [Fintype S] :
    IsRealizable ℚ (S ≃ S)

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/InverseGalois.lean, line 80.

InverseGalois.inverse_galois_problem.variants.complex_rational_functions

Solved: stated here without proof.

Every finite group is realisable over the field of rational functions with complex coefficients.

theorem inverse_galois_problem.variants.complex_rational_functions
    {G : Type*} [Fintype G] [Group G] :
    IsRealizable (RatFunc ℂ) G

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/InverseGalois.lean, line 90.

InverseGalois.inverse_galois_problem.variants.complex_function_field

Solved: stated here without proof.

Every finite group is realisable over the field of rational functions with coefficients K, where K is any algebraically closed field of characteristic 0.

theorem inverse_galois_problem.variants.complex_function_field
    {G K : Type*} [Field K] [IsAlgClosed K] [CharZero K] [Fintype G] [Group G] :
    IsRealizable (RatFunc K) G

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/InverseGalois.lean, line 100.

Sources
LeanInverseGalois.inverse_galois_problem · InverseGalois.inverse_galois_problem.variants.cyclic · InverseGalois.inverse_galois_problem.variants.abelian · InverseGalois.inverse_galois_problem.variants.symmetric_group · InverseGalois.inverse_galois_problem.variants.complex_rational_functions · InverseGalois.inverse_galois_problem.variants.complex_function_field

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.