Taxicab numbers to Woodall Primes

TheoremTaxicab numbers #

A taxicab number for natural numbers $k, m, n$ is the smallest number $x$ that can be expressed as a sum of $m$ positive $k$-th powers in at least $n$ distinct ways. The most famous taxicab number is $ 1729 = 1³ + 12³ = 9³ + 10³, $ also known as the Hardy–Ramanujan number.

However, a taxicab number is not known for $k=5$, $m=2$, and any $n ≥ 2$: No positive integer is known that can be written as the sum of two 5th powers in more than one way, and it is not known whether such a number exists.

In particular, it is not known whether there exists a taxicab number for $k=5$, $m=2$, and $n=2$.

References: - Wikipedia - Generalized taxicab number - OEIS taxicab cubes - OEIS taxicab 4th powers - OEIS taxicab conjecture

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

`Taxicab.taxicab_for_5_2_2`

Open: stated without proof.

Taxicab number for $k=5$, $m=2$, and $n=2$ is not known. Whether such a number exists is also not known.

theorem taxicab_for_5_2_2 : ∃ x : ℕ, IsTaxicabFor 5 2 2 x

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

`Taxicab.taxicab_for_5_2_n`

Open: stated without proof.

Taxicab number for $k=5$ and $m=2$ is not-known for any $n ≥ 2$. Whether such a number exists is also not known.

theorem taxicab_for_5_2_n : ∃ n : ℕ, n ≥ 2 ∧ (∃ x : ℕ, IsTaxicabFor 5 2 n x)

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

Sources

LeanTaxicab.taxicab_for_5_2_2 · Taxicab.taxicab_for_5_2_n

TheoremToronto spaces #

A Toronto space is a topological space which is homeomorphic to all of its subspaces of same cardinality.

It is conjectured that every T2, Toronto space is discrete. W.R. Brian proved that this holds under GCH.

References: - Wikipedia - The Toronto problem by W.R. Brian

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

`Toronto.DiscreteTopology.of_t2_of_torontoSpace`

Open: stated without proof.

Any T2, Toronto space is discrete.

theorem DiscreteTopology.of_t2_of_torontoSpace [T2Space X] [TorontoSpace X] :
    DiscreteTopology X

Category research open; AMS 54 General topology. Declared in FormalConjectures/Wikipedia/Toronto.lean, line 66.

Sources

LeanToronto.DiscreteTopology.of_t2_of_torontoSpace

TheoremThe total colouring conjecture (Behzad 1965, Vizing 1968)#

References: * Wikipedia * [Be65] Behzad, M. (1965). Graphs and their chromatic numbers. Ph.D. thesis, Michigan State University. * [Vi68] Vizing, V. G. (1968). "Some unsolved problems in graph theory." Uspekhi Mat. Nauk 23, pp. 117--134. * [Ko96] Kostochka, A. V. (1996). "The total chromatic number of any multigraph with maximum degree five is at most seven." Discrete Math. 162, pp. 199--214. * [MR98] Molloy, M. and Reed, B. (1998). "A bound on the total chromatic number." Combinatorica 18, pp. 241--280. * [Yap96] Yap, H. P. (1996). Total colourings of graphs. Lecture Notes in Mathematics 1623, Springer.

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

`TotalColoringConjecture.total_coloring_conjecture`

Open: stated without proof.

The total colouring conjecture (Behzad 1965, Vizing 1968).

Every finite simple graph $G$ has a total colouring with at most $\Delta(G) + 2$ colours, i.e. $\chi''(G) \le \Delta(G) + 2$, where $\Delta(G)$ is the maximum degree.

theorem total_coloring_conjecture :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      G.totalChromaticNumber ≤ G.maxDegree + 2

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

`TotalColoringConjecture.total_coloring_conjecture.variants.maxDegree_le_five`

Solved: stated here without proof.

Maximum degree at most 5 (Rosenfeld and Vijayaditya for $\Delta \le 3$; Kostochka for $\Delta = 4, 5$).

The conjecture holds for every graph of maximum degree at most $5$.

References: [Ko96], [Yap96].

theorem total_coloring_conjecture.variants.maxDegree_le_five
    {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hΔ : G.maxDegree ≤ 5) :
    G.totalChromaticNumber ≤ G.maxDegree + 2

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

`TotalColoringConjecture.total_coloring_conjecture.variants.complete_graph`

Solved: stated here without proof.

Complete graphs.

The total chromatic number of $K_n$ is $n$ for odd $n$ and $n + 1$ for even $n$ (see [Yap96]), so in particular the conjecture holds for complete graphs.

theorem total_coloring_conjecture.variants.complete_graph (n : ℕ) :
    (completeGraph (Fin n)).totalChromaticNumber ≤ (completeGraph (Fin n)).maxDegree + 2

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

`TotalColoringConjecture.total_coloring_conjecture.variants.molloy_reed`

Solved: stated here without proof.

Molloy–Reed (1998): $\chi''(G) \le \Delta(G) + C$ for an absolute constant $C$.

There is a constant $C$ (Molloy and Reed obtain $C = 10^{26}$) such that every graph satisfies $\chi''(G) \le \Delta(G) + C$.

Reference: [MR98].

theorem total_coloring_conjecture.variants.molloy_reed :
    ∃ C : ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      G.totalChromaticNumber ≤ G.maxDegree + C

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

Sources

LeanTotalColoringConjecture.total_coloring_conjecture · TotalColoringConjecture.total_coloring_conjecture.variants.maxDegree_le_five · TotalColoringConjecture.total_coloring_conjecture.variants.complete_graph · TotalColoringConjecture.total_coloring_conjecture.variants.molloy_reed

TheoremOpen questions on transcendence of numbers #

Reference: Wikipedia

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

The file states 22 research or textbook statements: 16 open, 5 solved and 1 textbook result.

`Transcendental.exp_add_pi_transcendental`

Open: stated without proof.

$e + \pi$ is transcendental.

theorem exp_add_pi_transcendental : Transcendental ℚ (exp 1 + π)

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 36.

`Transcendental.exp_mul_pi_transcendental`

Open: stated without proof.

$e\pi$ is transcendental.

theorem exp_mul_pi_transcendental : Transcendental ℚ (exp 1 * π)

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 43.

`Transcendental.exp_pow_pi_sq_transcendental`

Open: stated without proof.

$e^{\pi^2}$ is transcendental.

theorem exp_pow_pi_sq_transcendental : Transcendental ℚ (exp (π ^ 2))

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 50.

`Transcendental.exp_exp_transcendental`

Open: stated without proof.

$e^e$ is transcendental.

theorem exp_exp_transcendental : Transcendental ℚ (exp (exp 1))

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 57.

`Transcendental.pi_pow_exp_transcendental`

Open: stated without proof.

$\pi^e$ is transcendental.

theorem pi_pow_exp_transcendental : Transcendental ℚ (π ^ (exp 1))

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 64.

`Transcendental.pi_pow_sqrt_two_transcendental`

Open: stated without proof.

$\pi^{\sqrt{2}}$ is transcendental.

theorem pi_pow_sqrt_two_transcendental : Transcendental ℚ (π ^ √2)

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 71.

`Transcendental.pi_pow_pi_transcendental`

Open: stated without proof.

$\pi^{\pi}$ is transcendental.

theorem pi_pow_pi_transcendental : Transcendental ℚ (π ^ π)

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 78.

`Transcendental.pi_pow_pi_pow_pi_transcendental`

Open: stated without proof.

$\pi^{\pi^{\pi}}$ is transcendental.

theorem pi_pow_pi_pow_pi_transcendental : Transcendental ℚ (π ^ (π ^ π))

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 85.

`Transcendental.pi_pow_pi_pow_pi_pow_pi_transcendental`

Open: stated without proof.

$\pi^{\pi^{\pi^\pi}}$ is transcendental.

theorem pi_pow_pi_pow_pi_pow_pi_transcendental : Transcendental ℚ (π ^ (π ^ (π ^ π)))

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 92.

`Transcendental.pi_pow_pi_pow_pi_pow_pi_not_integer`

Open: stated without proof.

$\pi^{\pi^{\pi^\pi}}$ is not an integer.

This would follow from $\pi^{\pi^{\pi^\pi}}$ being transcendental, but this formulation is of interest in its own right, as it could in principle be proven by direct computation.

Reference: YouTube

theorem pi_pow_pi_pow_pi_pow_pi_not_integer : ¬ ∃ (n : ℤ), π ^ π ^ π ^ π = n

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 105.

`Transcendental.rlog_pi_transcendental`

Open: stated without proof.

$\log(\pi)$ is transcendental.

theorem rlog_pi_transcendental : Transcendental ℚ (log π)

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 112.

`Transcendental.rlog_rlog_two_transcendental`

Open: stated without proof.

$\log(\log(2))$ is transcendental.

theorem rlog_rlog_two_transcendental : Transcendental ℚ ((2 : ℝ).log.log)

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 119.

`Transcendental.sin_exp_transcendental`

Open: stated without proof.

$\sin(e)$ is transcendental.

theorem sin_exp_transcendental : Transcendental ℚ (Real.sin (exp 1))

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 126.

`Transcendental.exp_add_pi_or_exp_add_mul_transcendental`

Textbook result, stated without proof. A Lean proof is at https://github.com/Aegis-Omega/AEGIS-OMEGA/blob/6703489001e7374c5fd963dc5f8e98c34ea567cb/research/formal-conjectures-pilot/ExpTranscendence.lean#L149-L153.

At least one of $\pi + e$ and $\pi e$ is transcendental.

theorem exp_add_pi_or_exp_add_mul_transcendental :
    Transcendental ℚ (π + rexp 1) ∨ Transcendental ℚ (π * exp 1)

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

`Transcendental.transcendental_eulerMascheroniConstant_or_gompertzConstant`

Solved: stated here without proof.

At least one of the Euler–Mascheroni constant $\gamma$ and the Gompertz constant $\delta$ is transcendental.

[Ri12] Rivoal, T. (2012). On the arithmetic nature of the values of the gamma function, Euler's constant, and Gompertz's constant. Michigan Mathematical Journal, 61(2), 239–254.

theorem transcendental_eulerMascheroniConstant_or_gompertzConstant :
    Transcendental ℚ eulerMascheroniConstant ∨ Transcendental ℚ gompertzConstant

Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 147.

`Transcendental.transcendental_catalanConstant`

Open: stated without proof.

The Catalan constant $G$ is transcendental.

theorem transcendental_catalanConstant : Transcendental ℚ catalanConstant

Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 155.

`Transcendental.transcendental_gompertzConstant`

Open: stated without proof.

The Gompertz constant $\delta$ is transcendental.

theorem transcendental_gompertzConstant : Transcendental ℚ gompertzConstant

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 162.

`Transcendental.transcendental_gamma_one_div_two`

Solved: stated here without proof.

$\Gamma(1/2)$ is transcendental.

[Ch84] Chudnovsky, G. (1984). Contributions to the theory of transcendental numbers.

theorem transcendental_gamma_one_div_two : Transcendental ℚ (1 / 2 : ℝ).Gamma

Category research solved; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 171.

`Transcendental.transcendental_gamma_one_div_three`

Solved: stated here without proof.

$\Gamma(1/3)$ is transcendental.

[Ch84] Chudnovsky, G. (1984). Contributions to the theory of transcendental numbers.

theorem transcendental_gamma_one_div_three : Transcendental ℚ (1 / 3 : ℝ).Gamma

Category research solved; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 180.

`Transcendental.transcendental_gamma_one_div_four`

Solved: stated here without proof.

$\Gamma(1/4)$ is transcendental.

[Ch84] Chudnovsky, G. (1984). Contributions to the theory of transcendental numbers.

theorem transcendental_gamma_one_div_four : Transcendental ℚ (1 / 4 : ℝ).Gamma

Category research solved; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 189.

`Transcendental.transcendental_gamma_one_div_six`

Solved: stated here without proof.

$\Gamma(1/6)$ is transcendental.

[Ch84] Chudnovsky, G. (1984). Contributions to the theory of transcendental numbers.

theorem transcendental_gamma_one_div_six : Transcendental ℚ (1 / 6 : ℝ).Gamma

Category research solved; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 198.

`Transcendental.transcendental_gamma_one_div`

Open: stated without proof.

$\Gamma(1/n)$ for n ≥ 2 is transcendental.

theorem transcendental_gamma_one_div (n : ℕ) (hn : 2 ≤ n) : Transcendental ℚ (1 / n : ℝ).Gamma

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Transcendental.lean, line 205.

Sources

TheoremTuza's conjecture #

References: * Wikipedia * [Tu90] Tuza, Zs. (1990). "A conjecture on triangles of graphs." Graphs Combin. 6, pp. 373--380. * [Ha99] Haxell, P. E. (1999). "Packing and covering triangles in graphs." Discrete Math. 195, pp. 251--254.

Quoted from FormalConjectures/Wikipedia/TuzaConjecture.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 and 2 API statements, counted here but not shown.

`TuzaConjecture.tuza_conjecture`

Open: stated without proof.

Tuza's conjecture (1981): every finite graph $G$ satisfies $\tau(G) \le 2\nu(G)$, where $\tau(G)$ is its triangle covering number and $\nu(G)$ is its triangle packing number. The bound would be sharp, for example for $K_4$ and $K_5$.

theorem tuza_conjecture {V : Type} [Fintype V] (G : SimpleGraph V) :
    triangleCoverNumber G ≤ 2 * trianglePackingNumber G

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

`TuzaConjecture.tuza_conjecture.variants.haxell`

Solved: stated here without proof.

Haxell (1999): every finite graph satisfies $\tau(G) \le (66/23)\nu(G)$.

Reference: [Ha99].

theorem tuza_conjecture.variants.haxell {V : Type} [Fintype V] (G : SimpleGraph V) :
    (triangleCoverNumber G : ℝ) ≤ 66 / 23 * trianglePackingNumber G

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

Sources

LeanTuzaConjecture.tuza_conjecture · TuzaConjecture.tuza_conjecture.variants.haxell

TheoremTwin prime conjecture #

References: - Landau Problems Wikipedia Page - Twin Primes Conjecture Wikipedia Page

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

`TwinPrimes.twin_primes`

Open: stated without proof.

Are there infinitely many primes p such that p + 2 is prime?

theorem twin_primes :
    {p : ℕ | Prime p ∧ Prime (p + 2)}.Infinite

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

Sources

LeanTwinPrimes.twin_primes

TheoremUnion-closed sets conjecture #

Reference: Wikipedia

In this file, we: * state the conjecture * state three solved variants of the conjecture, without proof * prove two solved variants of the conjecture * prove the conjecture is sharp

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

`UnionClosed.union_closed`

Open: stated without proof.

For every finite union-closed family of sets, other than the family containing only the empty set, there exists an element that belongs to at least half of the sets in the family.

theorem union_closed
    [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A) :
    ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x}

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

`UnionClosed.union_closed.variants.yu`

Solved: stated here without proof.

Yu [Yu23] showed that the union-closed sets conjecture holds with a constant of approximately 0.38234 instead of 1/2. [Yu23] Yu, Lei (2023). "Dimension-free bounds for the union-closed sets conjecture". Entropy. 25 (5): 767.

theorem union_closed.variants.yu
    [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A) :
    ∃ i : n, (0.38234 : ℚ) * #A ≤ #{x ∈ A | i ∈ x}

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

`UnionClosed.union_closed.variants.univ_card`

Solved: stated here without proof.

Vuckovic and Zivkovic [Vu17] showed that the union-closed sets conjecture holds for set families whose universal set has cardinality at most 12. [Vu17] Vuckovic, Bojan; Zivkovic, Miodrag (2017). "The 12-Element Case of Frankl's Conjecture" (PDF). IPSI BGD Transactions on Internet Research. 13 (1): 65.

theorem union_closed.variants.univ_card
    [Fintype n] [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A)
    (h_card : Fintype.card n ≤ 12) :
    ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x}

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

`UnionClosed.union_closed.variants.family_card`

Solved: stated here without proof.

Roberts and Simpson [Ro10] showed that the union-closed sets conjecture holds for set families of size at most 46. Their method, however, combined with the result of [Vu17], further shows that it holds for #A ≤ 50 as well. [Ro10] Roberts, Ian; Simpson, Jamie (2010). "A note on the union-closed sets conjecture" (PDF). Australas. J. Combin. 47: 265–267. [Vu17] Vuckovic, Bojan; Zivkovic, Miodrag (2017). "The 12-Element Case of Frankl's Conjecture" (PDF). IPSI BGD Transactions on Internet Research. 13 (1): 65.

theorem union_closed.variants.family_card
    [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A)
    (hA : #A ≤ 50) :
    ∃ i : n, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x}

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

`UnionClosed.union_closed.variants.univ_card_two`

Proved here.

We can show the union-closed sets conjecture is true for the case where the universal set has cardinality 2, by brute force.

theorem union_closed.variants.univ_card_two (A : Finset (Finset (Fin 2)))
    (h_ne_singleton_empty : A ≠ {∅})
    (h_union_closed : IsUnionClosed A) :
    ∃ i, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x}

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

`UnionClosed.union_closed.variants.singleton_mem`

Proved here.

We can show the union-closed sets conjecture is true for the case where the set family contains some singleton.

theorem union_closed.variants.singleton_mem
    (h_union_closed : IsUnionClosed A)
    (i : n) (hi : {i} ∈ A) :
    ∃ i, (1 / 2 : ℚ) * #A ≤ #{x ∈ A | i ∈ x}

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

`UnionClosed.union_closed.variants.sharpness`

Proved here.

The union-closed sets conjecture is sharp in the sense that if we replace the constant 1/2 with any larger constant, then the conjecture fails.

theorem union_closed.variants.sharpness [Fintype n] (c : ℝ) (hc : 1 / 2 < c) :
    ¬ (∀ A : Finset (Finset n), A ≠ {∅} → IsUnionClosed A →
        ∃ i : n, c * #A ≤ #{x ∈ A | i ∈ x})

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

`UnionClosed.union_closed.variants.cardinality_even_of_union_closed_tight`

Open: stated without proof.

The union-closed sets conjecture is tight for a union-closed family A if the largest number of sets in A containing a common element is exactly half of the sets in A, that is, $\max_i |\{X \in A : i \in X\}| = |A| / 2$.

If the union-closed sets conjecture is tight for some family A then $|A| = 2^k$ for some $k$. This is the first part of Conjecture 3 in the reference below; its second part (that the family then contains the power set of a $k$-element set as a "submatrix") is not formalized here.

Reference: Conjecture 3 in https://www.nieuwarchief.nl/serie5/pdf/naw5-2023-24-4-225.pdf.

theorem union_closed.variants.cardinality_even_of_union_closed_tight
    [Nonempty n]
    (h_ne_singleton_empty : A ≠ {∅})
    (h_ne_empty : A ≠ ∅)
    (h_union_closed : IsUnionClosed A)
    (h_tight : IsGreatest (Set.range fun i : n => (#{x ∈ A | i ∈ x} : ℚ)) ((1 / 2 : ℚ) * #A)) :
    ∃ k, #A = 2 ^ k

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

Sources

LeanUnionClosed.union_closed · UnionClosed.union_closed.variants.yu · UnionClosed.union_closed.variants.univ_card · UnionClosed.union_closed.variants.family_card · UnionClosed.union_closed.variants.univ_card_two · UnionClosed.union_closed.variants.singleton_mem · UnionClosed.union_closed.variants.sharpness · UnionClosed.union_closed.variants.cardinality_even_of_union_closed_tight

TheoremVaught conjecture #

Reference: Wikipedia

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

`VaughtConjecture.vaught_conjecture`

Open: stated without proof.

The Vaught conjecture states that for a countable language L and a complete L-Theory T the number of countable models of T (up to isomorphism) is finite, $\aleph_0$ or $2^{\aleph_0}$.

theorem vaught_conjecture {L : FirstOrder.Language} (hL : Countable L.Symbols)
                          {T : L.Theory} (hT : T.IsComplete) :
  numberOfCountableModels T ≤ Cardinal.aleph0 ∨ numberOfCountableModels T = Cardinal.continuum

Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/Wikipedia/VaughtConjecture.lean, line 44.

Sources

LeanVaughtConjecture.vaught_conjecture

TheoremVizing's conjecture (1968)#

References: * Wikipedia * [Vi68] Vizing, V. G. (1968). "Some unsolved problems in graph theory." Uspekhi Mat. Nauk 23, pp. 117--134. * [ClSu00] Clark, W. E. and Suen, S. (2000). "An inequality related to Vizing's conjecture." Electron. J. Combin. 7, N4. * [SuTa12] Suen, S. and Tarr, J. (2012). "An improved inequality related to Vizing's conjecture." Electron. J. Combin. 19, P8. * [BDGHHKR12] Brešar, B., Dorbec, P., Goddard, W., Hartnell, B. L., Henning, M. A., Klavžar, S. and Rall, D. F. (2012). "Vizing's conjecture: a survey and recent results." J. Graph Theory 69, pp. 46--76.

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

`VizingConjecture.vizing_conjecture`

Open: stated without proof.

Vizing's conjecture (1968).

For all finite simple graphs $G$ and $H$, the domination number of the Cartesian (box) product satisfies $\gamma(G \,\square\, H) \ge \gamma(G)\,\gamma(H)$.

theorem vizing_conjecture :
    ∀ {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
      (G : SimpleGraph α) (H : SimpleGraph β),
      G.dominationNumber * H.dominationNumber ≤ (G □ H).dominationNumber

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

`VizingConjecture.vizing_conjecture.variants.clark_suen`

Solved: stated here without proof.

The Clark–Suen inequality (2000).

For all finite simple graphs $G$ and $H$, $\gamma(G \,\square\, H) \ge \tfrac12\,\gamma(G)\,\gamma(H)$; that is, Vizing's conjecture holds up to a factor of $2$.

Reference: [ClSu00].

theorem vizing_conjecture.variants.clark_suen
    {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
    (G : SimpleGraph α) (H : SimpleGraph β) :
    G.dominationNumber * H.dominationNumber ≤ 2 * (G □ H).dominationNumber

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

`VizingConjecture.vizing_conjecture.variants.suen_tarr`

Solved: stated here without proof.

The Suen–Tarr inequality (2012).

For all finite simple graphs $G$ and $H$, $\gamma(G \,\square\, H) \ge \tfrac12\,\gamma(G)\,\gamma(H) + \tfrac12\min\{\gamma(G), \gamma(H)\}$, improving the Clark–Suen bound.

Reference: [SuTa12].

theorem vizing_conjecture.variants.suen_tarr
    {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
    (G : SimpleGraph α) (H : SimpleGraph β) :
    G.dominationNumber * H.dominationNumber + min G.dominationNumber H.dominationNumber ≤
      2 * (G □ H).dominationNumber

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

`VizingConjecture.vizing_conjecture.variants.dominationNumber_eq_one`

Proved here.

Vizing's conjecture when γ(H) = 1.

If H has a dominating vertex, so that $\gamma(H) = 1$, then Vizing's inequality reduces to $\gamma(G) \le \gamma(G \,\square\, H)$, which is the projection bound dominationNumber_le_dominationNumber_boxProd. This is the simplest of the known cases of the conjecture (see [BDGHHKR12]).

theorem vizing_conjecture.variants.dominationNumber_eq_one
    {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
    (G : SimpleGraph α) (H : SimpleGraph β) (hH : H.dominationNumber = 1) :
    G.dominationNumber * H.dominationNumber ≤ (G □ H).dominationNumber

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

Sources

LeanVizingConjecture.vizing_conjecture · VizingConjecture.vizing_conjecture.variants.clark_suen · VizingConjecture.vizing_conjecture.variants.suen_tarr · VizingConjecture.vizing_conjecture.variants.dominationNumber_eq_one

LemmaInfinitude of Wall–Sun–Sun primes #

References: - Wikipedia - [EJ10] A.-S. Elsenhans and J. Jahnel, The Fibonacci sequence modulo $p^2$ – An investigation by computer for $p < 10^{14}$, arXiv:1006.0824

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

The file states 11 research or textbook statements: 3 open and 8 textbook results. It also has 1 test statement, counted here but not shown.

`QuadraticAlgebra.discr_rat_of_modEq_one`

Textbook result, stated without proof.

The discriminant of ℚ[√d] for d ≥ 2 squarefree congruent to 1 mod 4 is d.

lemma discr_rat_of_modEq_one (hd₄ : d ≡ 1 [ZMOD 4]) : discr (QuadraticAlgebra ℚ d 0) = d

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

`QuadraticAlgebra.discr_rat_of_not_modEq_one`

Textbook result, stated without proof.

The discriminant of ℚ[√d] for d ≥ 2 squarefree not congruent to 1 mod 4 is 4 * d.

lemma discr_rat_of_not_modEq_one (hd₄ : ¬ d ≡ 1 [ZMOD 4]) :
    discr (QuadraticAlgebra ℚ d 0) = 4 * d

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

`Algebra.exists_quadraticAlgebra_of_isQuadraticExtension`

Textbook result, stated without proof.

A quadratic algebra L over a field K is isomorphic to the explicit quadratic algebra QuadraticAlgebra K a b for some a b : K.

lemma exists_quadraticAlgebra_of_isQuadraticExtension [IsQuadraticExtension K L] :
    ∃ a b, Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b)

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

`Algebra.isQuadraticExtension_iff_exists_quadraticAlgebra`

Textbook result, stated without proof.

An algebra L is quadratic over a field K iff it is isomorphic to the explicit quadratic algebra QuadraticAlgebra K a b for some a b : K.

lemma isQuadraticExtension_iff_exists_quadraticAlgebra :
    IsQuadraticExtension K L ↔ ∃ a b, Nonempty (L ≃ₐ[K] QuadraticAlgebra K a b)

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

`NumberField.exists_quadraticAlgebra_of_isQuadraticExtension`

Textbook result, stated without proof.

A quadratic number field K is isomorphic to the explicit quadratic field QuadraticAlgebra ℚ d 0 for some squarefree d : ℤ not equal to 1.

lemma exists_quadraticAlgebra_of_isQuadraticExtension [IsQuadraticExtension ℚ K] :
    ∃ d ≠ (1 : ℤ), Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ d 0)

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

`NumberField.isQuadraticExtension_iff_exists_quadraticAlgebra`

Textbook result, stated without proof.

A number field K is quadratic iff it is isomorphic to the explicit quadratic field QuadraticAlgebra ℚ d 0 for some squarefree d : ℤ not equal to 1.

lemma isQuadraticExtension_iff_exists_quadraticAlgebra :
    IsQuadraticExtension ℚ K ↔
      ∃ d ≠ (1 : ℤ), Squarefree d ∧ Nonempty (K ≃+* QuadraticAlgebra ℚ d 0)

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

`NumberField.isFundamentalDiscr_iff_exists_discr_quadraticAlgebra`

Textbook result, proved here.

An integer D is a fundamental discriminant iff it is the discriminant of the explicit quadratic field QuadraticAlgebra ℚ d 0 for some squarefree d : ℤ not equal to 1.

lemma isFundamentalDiscr_iff_exists_discr_quadraticAlgebra {D : ℤ} :
    IsFundamentalDiscr D ↔ ∃ (d : ℤ) (_ : Fact <| d ≠ 1) (_ : Fact <| Squarefree d),
      discr (QuadraticAlgebra ℚ d 0) = D

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

`NumberField.isFundamentalDiscr_iff_exists_discr_numberField`

Textbook result, proved here.

An integer D is a fundamental discriminant iff it is the discriminant of some number field.

lemma isFundamentalDiscr_iff_exists_discr_numberField {D : ℤ} :
    IsFundamentalDiscr D ↔
      ∃ (K : Type) (_ : Field K) (_ : NumberField K), IsQuadraticExtension ℚ K ∧ discr K = D

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

`WallSunSun.exists_isWallSunSunPrime`

Open: stated without proof.

A prime $p$ is a Wall–Sun–Sun prime if and only if $L_p \equiv 1 \pmod{p^2}$, where $L_p$ is the $p$-th Lucas number. It is conjectured that there is at least one Wall–Sun–Sun prime.

theorem exists_isWallSunSunPrime : ∃ p, IsWallSunSunPrime p

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

`WallSunSun.infinite_isWallSunSunPrime`

Open: stated without proof.

A prime $p$ is a Wall–Sun–Sun prime if and only if $L_p \equiv 1 \pmod{p^2}$, where $L_p$ is the $p$-th Lucas number. It is conjectured that there are infinitely many Wall-Sun-Sun primes.

theorem infinite_isWallSunSunPrime : {p : ℕ | IsWallSunSunPrime p}.Infinite

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

`WallSunSun.infinite_isWallSunSunPrime_of_disc_eq`

Open: stated without proof.

Let $K$ be a real quadratic field of discriminant $D$ and let $\varepsilon$ be a fundamental unit of $K$. Following [EJ10, Remark 2.2.8], an odd prime $p \nmid D$ is a Wall–Sun–Sun prime for $K$ if, in $\mathcal{O}_K$, $\varepsilon^{p-1} \equiv 1 \pmod{p^2}$ when $\left(\tfrac{D}{p}\right) = 1$, and $\varepsilon^{2p+2} \equiv 1 \pmod{p^2}$ when $\left(\tfrac{D}{p}\right) = -1$. Both exponents are even, so the condition does not depend on the choice of $\varepsilon$, and it is equivalent to asking the same congruence for every unit of $K$. For $K = \mathbb{Q}(\sqrt{5})$ and $\varepsilon = \frac{1 + \sqrt{5}}{2}$ these are the classical Wall–Sun–Sun primes other than $2$ and $5$ [EJ10, Proposition 2.2.6].

It is conjectured that for every fundamental discriminant $D \neq 1$ there are infinitely many Wall–Sun–Sun primes with discriminant $D$ (Wikipedia; [EJ10, §4.1] gives the heuristic for $\mathbb{Q}(\sqrt{5})$). It is stated here for $D > 0$ only. Wikipedia's sentence also covers $D < 0$, but [EJ10] gives the definition above only for real quadratic fields, and its literal extension to imaginary quadratic fields is degenerate: there every unit is a root of unity of order dividing $4$ or $6$, and that order divides the relevant exponent $p - 1$ or $2p + 2$ for every odd prime $p \nmid D$.

theorem infinite_isWallSunSunPrime_of_disc_eq {K : Type*} [Field K] [NumberField K]
    [IsQuadraticExtension ℚ K] [IsTotallyReal K] {D : ℤ} (hD : discr K = D) :
    {p : ℕ | p.Prime ∧ Odd p ∧ ¬ (p : ℤ) ∣ D ∧ ∀ ε : (𝓞 K)ˣ,
      (p : 𝓞 K) ^ 2 ∣ (ε : 𝓞 K) ^ (if J(D | p) = 1 then p - 1 else 2 * p + 2) - 1}.Infinite

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

Sources

LeanQuadraticAlgebra.discr_rat_of_modEq_one · QuadraticAlgebra.discr_rat_of_not_modEq_one · Algebra.exists_quadraticAlgebra_of_isQuadraticExtension · Algebra.isQuadraticExtension_iff_exists_quadraticAlgebra · NumberField.exists_quadraticAlgebra_of_isQuadraticExtension · NumberField.isQuadraticExtension_iff_exists_quadraticAlgebra · NumberField.isFundamentalDiscr_iff_exists_discr_quadraticAlgebra · NumberField.isFundamentalDiscr_iff_exists_discr_numberField · WallSunSun.exists_isWallSunSunPrime · WallSunSun.infinite_isWallSunSunPrime · WallSunSun.infinite_isWallSunSunPrime_of_disc_eq

TheoremCan a prime $p$ satisfy $2^{p-1} \equiv 1 \pmod{p^2}$ and $3^{p-1} \equiv 1 \pmod{p^2}$?#

A prime $p$ with $2^{p-1} \equiv 1 \pmod{p^2}$ is a Wieferich prime (the only known examples are $1093$ and $3511$). A prime $p$ with $3^{p-1} \equiv 1 \pmod{p^2}$ is a Mirimanoff prime (the only known examples are $11$ and $1006003$). It is an open question whether a prime can satisfy both congruences simultaneously. Lenstra gave a heuristic argument against this.

References: * Wikipedia, List of unsolved problems in mathematics * Wikipedia, Wieferich prime * J. B. Dobson, On Lerch's formula for the Fermat quotient * F. G. Dorais and D. Klyve, A Wieferich prime search up to $6.7 \times 10^{15}$, J. Integer Seq. 14 (2011), Article 11.9.2. * OEIS A001220 (Wieferich primes) * OEIS A014127 (Mirimanoff primes)

Quoted from FormalConjectures/Wikipedia/WieferichMirimanoffPrime.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 4 test statements, counted here but not shown.

`WieferichMirimanoffPrime.exists_isWieferichPrime_and_isMirimanoffPrime`

Open: stated without proof.

Can a prime $p$ satisfy $2^{p-1} \equiv 1 \pmod{p^2}$ and $3^{p-1} \equiv 1 \pmod{p^2}$ simultaneously? That is, does there exist a prime $p$ that is both a Wieferich prime and a Mirimanoff prime? Wikipedia's list of unsolved problems poses this question, citing J. B. Dobson, On Lerch's formula for the Fermat quotient. Lenstra gave a heuristic argument against the existence of such a prime (see Dobson, Section 9).

theorem exists_isWieferichPrime_and_isMirimanoffPrime :
    ∃ p : ℕ, IsWieferichPrime p ∧ IsMirimanoffPrime p

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

`WieferichMirimanoffPrime.isMirimanoffPrime_iff`

Open: stated without proof.

Are $11$ and $1006003$ the only Mirimanoff primes? They are the only known ones: Dorais and Klyve found no other below $9.7 \times 10^{14}$.

theorem isMirimanoffPrime_iff :
    ∀ p, IsMirimanoffPrime p ↔ p = 11 ∨ p = 1006003

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

Sources

LeanWieferichMirimanoffPrime.exists_isWieferichPrime_and_isMirimanoffPrime · WieferichMirimanoffPrime.isMirimanoffPrime_iff

TheoremWieferich primes #

A Wieferich prime is a prime $p$ with $2^{p-1} \equiv 1 \pmod{p^2}$. The only known examples are $1093$ and $3511$. It is conjectured that there are infinitely many Wieferich primes; a heuristic argument suggests that the number of Wieferich primes up to $x$ grows like $\log \log x$.

More generally, a prime $p$ is a Wieferich prime to base $a$ if $a^{p-1} \equiv 1 \pmod{p^2}$. Wikipedia's list of unsolved problems also asks whether there are infinitely many Wieferich primes to every base $a > 0$, and whether there is any Wieferich prime to base $47$. It is also not known whether there is any Wieferich prime besides $1093$ and $3511$.

References: * Wikipedia, List of unsolved problems in mathematics * Wikipedia, Wieferich prime * OEIS A001220 * P. Ribenboim, Die Welt der Primzahlen, 2nd ed., Springer (2006), pp. 242–243. * PrimeGrid, Wieferich and Wall–Sun–Sun Prime Search

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

`WieferichPrime.infinite_isWieferichPrime`

Open: stated without proof.

There are infinitely many Wieferich primes.

theorem infinite_isWieferichPrime : {p : ℕ | IsWieferichPrime p}.Infinite

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

`WieferichPrime.isWieferichPrime_iff`

Open: stated without proof.

Are $1093$ and $3511$ the only Wieferich primes? They are the only known ones: PrimeGrid's search, completed in 2022, shows that any other Wieferich prime exceeds $2^{64}$. On the other hand, the heuristic count of $\log \log x$ Wieferich primes up to $x$ predicts that there are infinitely many, see infinite_isWieferichPrime.

theorem isWieferichPrime_iff :
    ∀ p, IsWieferichPrime p ↔ p = 1093 ∨ p = 3511

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

`WieferichPrime.infinite_isWieferichPrimeBase`

Open: stated without proof.

For any given integer $a > 0$, are there infinitely many primes $p$ such that $a^{p-1} \equiv 1 \pmod{p^2}$? The case $a = 1$ is trivial, since every prime qualifies (isWieferichPrimeBase_one_iff). So is the case $a = 0$ under our definition (isWieferichPrimeBase_zero_iff), which is why the source's restriction to $a > 0$ is dropped.

theorem infinite_isWieferichPrimeBase :
    ∀ a : ℕ, {p : ℕ | IsWieferichPrimeBase a p}.Infinite

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

`WieferichPrime.exists_isWieferichPrimeBase_47`

Open: stated without proof.

Are there any Wieferich primes to base $47$? None is currently known.

theorem exists_isWieferichPrimeBase_47 : ∃ p, IsWieferichPrimeBase 47 p

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

Sources

LeanWieferichPrime.infinite_isWieferichPrime · WieferichPrime.isWieferichPrime_iff · WieferichPrime.infinite_isWieferichPrimeBase · WieferichPrime.exists_isWieferichPrimeBase_47

TheoremWilson primes #

A Wilson prime is a prime $p$ for which $p^2$ divides $(p-1)!+1$. The only known examples are $5$, $13$, and $563$. It is conjectured that infinitely many Wilson primes exist.

References: * Wikipedia, Wilson prime * OEIS A007540 * E. Costa, R. Gerbicz, and D. Harvey, A search for Wilson primes

Quoted from FormalConjectures/Wikipedia/WilsonPrime.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 4 test statements, counted here but not shown.

`WilsonPrime.infinitely_many_wilson_primes`

Open: stated without proof.

There are infinitely many Wilson primes.

theorem infinitely_many_wilson_primes : Set.Infinite {p : ℕ | IsWilsonPrime p}

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

Sources

LeanWilsonPrime.infinitely_many_wilson_primes

TheoremWolstenholme Prime #

Reference: Wikipedia

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

`WolstenholmePrime.wolstenholme_theorem`

Textbook result, stated without proof. A Lean proof is at https://github.com/mo271/formal-conjectures/blob/d833ed31d82693f10bed7a4c9ac329545b556a03/FormalConjectures/Wikipedia/WolstenholmePrime.lean#L34.

Wolstenholme's theorem states that any prime $p > 3$ satisfies $\binom{2p-1}{p-1} \equiv 1 (\pmod{p^3})$.

Formal proof linked here provided by AlphaProof. Reference: Wikipedia

theorem wolstenholme_theorem (p : ℕ) (h : p > 3) (hp : Nat.Prime p) :
    (2 * p - 1).choose (p - 1) ≡ 1 [MOD p ^ 3]

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

`WolstenholmePrime.wolstenholme_bernoulli`

Textbook result, stated without proof.

Equivalently, a prime $p > 7$ is a Wolstenholme prime if it divides the numerator of the Bernoulli number $B_{p-3}$.

theorem wolstenholme_bernoulli (p : ℕ) : IsWolstenholmePrime p ↔
    (p > 7) ∧ Nat.Prime p ∧ ↑p ∣ (bernoulli' (p - 3)).num

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

`WolstenholmePrime.wolstenholme_harmonic`

Textbook result, stated without proof.

Another equivalent definition is that a prime $p > 7$ is a Wolstenholme prime if it $p^3$ divides the numerator of the harmonic number $H_{p-1}$.

theorem wolstenholme_harmonic (p : ℕ) : IsWolstenholmePrime p ↔
    (p > 7) ∧ Nat.Prime p ∧ ↑(p ^ 3) ∣ (harmonic (p - 1)).num

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

`WolstenholmePrime.wolstenholme_prime_infinite`

Open: stated without proof.

It is conjectured that there are infinitely many Wolstenholme primes.

Reference: Wikipedia

theorem wolstenholme_prime_infinite :
    {p : ℕ | IsWolstenholmePrime p}.Infinite

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

Sources

LeanWolstenholmePrime.wolstenholme_theorem · WolstenholmePrime.wolstenholme_bernoulli · WolstenholmePrime.wolstenholme_harmonic · WolstenholmePrime.wolstenholme_prime_infinite

TheoremWoodall Primes #

References: * Wikipedia/Woodall Number * A2234

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

`WoodallPrimes.infinitely_many_woodall_primes`

Open: stated without proof.

There are infinitely many prime numbers of the form k * 2 ^ k - 1 for k > 1.

theorem infinitely_many_woodall_primes : {k : ℕ | 1 < k ∧ (k * 2 ^ k - 1).Prime}.Infinite

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

Sources

LeanWoodallPrimes.infinitely_many_woodall_primes

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Taxicab numbers to Woodall Primes

TheoremTaxicab numbers#

Taxicab.taxicab_for_5_2_2

Taxicab.taxicab_for_5_2_n

Sources

TheoremToronto spaces#

Toronto.DiscreteTopology.of_t2_of_torontoSpace

Sources

TheoremThe total colouring conjecture (Behzad 1965, Vizing 1968)#

TotalColoringConjecture.total_coloring_conjecture

TotalColoringConjecture.total_coloring_conjecture.variants.maxDegree_le_five

TotalColoringConjecture.total_coloring_conjecture.variants.complete_graph

TotalColoringConjecture.total_coloring_conjecture.variants.molloy_reed

Sources

TheoremOpen questions on transcendence of numbers#

Transcendental.exp_add_pi_transcendental

Transcendental.exp_mul_pi_transcendental

Transcendental.exp_pow_pi_sq_transcendental

Transcendental.exp_exp_transcendental

Transcendental.pi_pow_exp_transcendental

Transcendental.pi_pow_sqrt_two_transcendental

Transcendental.pi_pow_pi_transcendental

Transcendental.pi_pow_pi_pow_pi_transcendental

Transcendental.pi_pow_pi_pow_pi_pow_pi_transcendental

Transcendental.pi_pow_pi_pow_pi_pow_pi_not_integer

Transcendental.rlog_pi_transcendental

Transcendental.rlog_rlog_two_transcendental

Transcendental.sin_exp_transcendental

Transcendental.exp_add_pi_or_exp_add_mul_transcendental

Transcendental.transcendental_eulerMascheroniConstant_or_gompertzConstant

Transcendental.transcendental_catalanConstant

Transcendental.transcendental_gompertzConstant

Transcendental.transcendental_gamma_one_div_two

Transcendental.transcendental_gamma_one_div_three

Transcendental.transcendental_gamma_one_div_four

Transcendental.transcendental_gamma_one_div_six

Transcendental.transcendental_gamma_one_div

Sources

TheoremTuza's conjecture#

TuzaConjecture.tuza_conjecture

TuzaConjecture.tuza_conjecture.variants.haxell

Sources

TheoremTwin prime conjecture#

TwinPrimes.twin_primes

Sources

TheoremUnion-closed sets conjecture#

UnionClosed.union_closed

UnionClosed.union_closed.variants.yu

UnionClosed.union_closed.variants.univ_card

UnionClosed.union_closed.variants.family_card

UnionClosed.union_closed.variants.univ_card_two

UnionClosed.union_closed.variants.singleton_mem

UnionClosed.union_closed.variants.sharpness

UnionClosed.union_closed.variants.cardinality_even_of_union_closed_tight

Sources

TheoremVaught conjecture#

VaughtConjecture.vaught_conjecture

Sources

TheoremVizing's conjecture (1968)#

VizingConjecture.vizing_conjecture

VizingConjecture.vizing_conjecture.variants.clark_suen

VizingConjecture.vizing_conjecture.variants.suen_tarr

VizingConjecture.vizing_conjecture.variants.dominationNumber_eq_one

Sources

LemmaInfinitude of Wall–Sun–Sun primes#

QuadraticAlgebra.discr_rat_of_modEq_one

QuadraticAlgebra.discr_rat_of_not_modEq_one

Algebra.exists_quadraticAlgebra_of_isQuadraticExtension

Algebra.isQuadraticExtension_iff_exists_quadraticAlgebra

NumberField.exists_quadraticAlgebra_of_isQuadraticExtension

NumberField.isQuadraticExtension_iff_exists_quadraticAlgebra

NumberField.isFundamentalDiscr_iff_exists_discr_quadraticAlgebra

NumberField.isFundamentalDiscr_iff_exists_discr_numberField

WallSunSun.exists_isWallSunSunPrime

WallSunSun.infinite_isWallSunSunPrime

WallSunSun.infinite_isWallSunSunPrime_of_disc_eq

Sources

TheoremCan a prime \(p\) satisfy \(2^{p-1} \equiv 1 \pmod{p^2}\) and \(3^{p-1} \equiv 1 \pmod{p^2}\)?#

WieferichMirimanoffPrime.exists_isWieferichPrime_and_isMirimanoffPrime

WieferichMirimanoffPrime.isMirimanoffPrime_iff

TheoremTaxicab numbers #

`Taxicab.taxicab_for_5_2_2`

`Taxicab.taxicab_for_5_2_n`

TheoremToronto spaces #

`Toronto.DiscreteTopology.of_t2_of_torontoSpace`

`TotalColoringConjecture.total_coloring_conjecture`

`TotalColoringConjecture.total_coloring_conjecture.variants.maxDegree_le_five`

`TotalColoringConjecture.total_coloring_conjecture.variants.complete_graph`

`TotalColoringConjecture.total_coloring_conjecture.variants.molloy_reed`

TheoremOpen questions on transcendence of numbers #

`Transcendental.exp_add_pi_transcendental`

`Transcendental.exp_mul_pi_transcendental`

`Transcendental.exp_pow_pi_sq_transcendental`

`Transcendental.exp_exp_transcendental`

`Transcendental.pi_pow_exp_transcendental`

`Transcendental.pi_pow_sqrt_two_transcendental`

`Transcendental.pi_pow_pi_transcendental`

`Transcendental.pi_pow_pi_pow_pi_transcendental`

`Transcendental.pi_pow_pi_pow_pi_pow_pi_transcendental`

`Transcendental.pi_pow_pi_pow_pi_pow_pi_not_integer`

`Transcendental.rlog_pi_transcendental`

`Transcendental.rlog_rlog_two_transcendental`

`Transcendental.sin_exp_transcendental`

`Transcendental.exp_add_pi_or_exp_add_mul_transcendental`

`Transcendental.transcendental_eulerMascheroniConstant_or_gompertzConstant`

`Transcendental.transcendental_catalanConstant`

`Transcendental.transcendental_gompertzConstant`

`Transcendental.transcendental_gamma_one_div_two`

`Transcendental.transcendental_gamma_one_div_three`

`Transcendental.transcendental_gamma_one_div_four`

`Transcendental.transcendental_gamma_one_div_six`

`Transcendental.transcendental_gamma_one_div`

TheoremTuza's conjecture #

`TuzaConjecture.tuza_conjecture`

`TuzaConjecture.tuza_conjecture.variants.haxell`

TheoremTwin prime conjecture #

`TwinPrimes.twin_primes`

TheoremUnion-closed sets conjecture #

`UnionClosed.union_closed`

`UnionClosed.union_closed.variants.yu`

`UnionClosed.union_closed.variants.univ_card`

`UnionClosed.union_closed.variants.family_card`

`UnionClosed.union_closed.variants.univ_card_two`

`UnionClosed.union_closed.variants.singleton_mem`

`UnionClosed.union_closed.variants.sharpness`

`UnionClosed.union_closed.variants.cardinality_even_of_union_closed_tight`

TheoremVaught conjecture #

`VaughtConjecture.vaught_conjecture`

`VizingConjecture.vizing_conjecture`

`VizingConjecture.vizing_conjecture.variants.clark_suen`

`VizingConjecture.vizing_conjecture.variants.suen_tarr`

`VizingConjecture.vizing_conjecture.variants.dominationNumber_eq_one`

LemmaInfinitude of Wall–Sun–Sun primes #

`QuadraticAlgebra.discr_rat_of_modEq_one`

`QuadraticAlgebra.discr_rat_of_not_modEq_one`

`Algebra.exists_quadraticAlgebra_of_isQuadraticExtension`

`Algebra.isQuadraticExtension_iff_exists_quadraticAlgebra`

`NumberField.exists_quadraticAlgebra_of_isQuadraticExtension`

`NumberField.isQuadraticExtension_iff_exists_quadraticAlgebra`

`NumberField.isFundamentalDiscr_iff_exists_discr_quadraticAlgebra`

`NumberField.isFundamentalDiscr_iff_exists_discr_numberField`

`WallSunSun.exists_isWallSunSunPrime`

`WallSunSun.infinite_isWallSunSunPrime`

`WallSunSun.infinite_isWallSunSunPrime_of_disc_eq`

`WieferichMirimanoffPrime.exists_isWieferichPrime_and_isMirimanoffPrime`

`WieferichMirimanoffPrime.isMirimanoffPrime_iff`

TheoremWieferich primes #

`WieferichPrime.infinite_isWieferichPrime`

`WieferichPrime.isWieferichPrime_iff`

`WieferichPrime.infinite_isWieferichPrimeBase`

`WieferichPrime.exists_isWieferichPrimeBase_47`

TheoremWilson primes #

`WilsonPrime.infinitely_many_wilson_primes`

TheoremWolstenholme Prime #

`WolstenholmePrime.wolstenholme_theorem`

`WolstenholmePrime.wolstenholme_bernoulli`

`WolstenholmePrime.wolstenholme_harmonic`

`WolstenholmePrime.wolstenholme_prime_infinite`

TheoremWoodall Primes #

`WoodallPrimes.infinitely_many_woodall_primes`