Formal Conjectures is an open repository, started by Google DeepMind, of conjectures stated in Lean 4 with Mathlib. Every open problem from it that we import keeps its exact Lean statement, so a proof submitted here is checked by the Lean kernel against that statement. The collection covers Erdős problems, OEIS conjectures, Ben Green's open problems, Wikipedia's lists of unsolved problems, MathOverflow questions and more.
Source: google-deepmind/formal-conjectures. Licence: Apache License 2.0.
103 is conjectured to be the smallest number such that the Reverse and Add! algorithm in base 3 does not lead to a palindrome. Its trajectory is conjectured to never reach a palindrome.
It is conjectured that this trajectory does not close on itself.
Terms are squares at only(?) three values of n = 3, 6, 4072: corresponding terms are 6^2, 13^2, and 15735^2.
Conjecture (i): a(n) > 0 for all n > 2.
OEIS A331631 states: The sequence is conjectured to be a permutation of the positive integers (see the Crossrefs section).
Is the score a(n) > 0 for some n > 250000?
Tuza's conjecture (1981): every finite graph G satisfies τ(G) ≤ 2ν(G), where τ(G) is its triangle covering number and ν(G) is its triangle packing number. The bound would be sharp, for example for K_4 and K_5.
Are there infinitely many primes p such that p + 2 is prime?
Conjecture: There is always one such k for each n > 0 such that (3^n - k) 2^n - 1 and (3^n - k) 2^n + 1 are a twin prime pair.
TxGraffiti Conjecture 2: for every connected graph G with Δ(G) ≤ 3 and G ≠ K_4, Z(G) ≤ α(G) + 1. This conjecture is open.
TxGraffiti Conjecture 3: for every r-regular graph G (r ≥ 1), i(G) ≤ μ^(G). This conjecture is open**.
Conjecture: a(n) > 0 for all n > 5 with n not equal to 13.
If n = ab is a crystal, then there are no other pairs of positive integers c, d > 1, different from the couple a, b, such that n = cd and B(c, d) ∈ ℕ, i.e., the components of the crystals are unique.
a(28341) is divisible by 283411^2. What is the next n such that a(n) is not squarefree?
Conjecture (i): a(n) > 0 for all n > 3.
OEIS A181391 conjectures: "every number eventually appears."
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.
Every convex set in ℝ^3 has VC_2 dimension at most 2.
Vizing's conjecture (1968). For all finite simple graphs G and H, the domination number of the Cartesian (box) product satisfies γ(G square H) ≥ γ(G) γ(H).
It is conjectured that a(n) is always positive (Conjecture 1.1 of Sun (2009)).
Conjecture: a(n) > 0 for all n > 1.
Conjecture: a(n) > 0 for all n > 5.
Conjecture: a(n) > 0 for all n > 1.
Conjecture (i), part 1: a(n) > 0 for all n > 2.
Conjecture: For any positive integer m, every nonnegative integer n can be written as ⌊ T(x)/m ⌋ + ⌊ T(y)/m ⌋ + ⌊ T(z)/m ⌋ with x, y, z nonnegative integers.
Problem 4.2. Let Ω ⊂ ℝ be a finite union of three or more intervals. If Ω weakly tiles its complement, must it also tile its complement properly?
There are infinitely many Wieferich primes.
There are infinitely many Wilson primes.
Conjecture: for n > 3, gcd(n, a(n-1)) = A089026(n). - Amiram Eldar and Thomas Ordowski, Jul 28 2019
It is conjectured that there are infinitely many Wolstenholme primes. Reference: Wikipedia
There are infinitely many prime numbers of the form k * 2 ^ k - 1 for k > 1.
WOWII Conjecture 100 (status O): For a simple connected graph G, α(G) ≤ ⌈(max_v l(v) + 0.5 · degreeL2Norm(Gᶜ)) / 2⌉ where α(G) = G.indepNum is the independence number, max_v l(v) is the maximum over all vertices of the independence number of the neighbourhood (in G), and degreeL2Norm(Gᶜ) is the…
WOWII Conjecture 133: For a simple connected graph G, path(G) ≥ rad(G) + (avg_v l(v))^cC_4(G), where path(G) is the path number of the graph (number of vertices of a largest induced path), rad(G) is the radius (minimum eccentricity, as a natural number), avg_v l(v) = l(G) is the average…
WOWII Conjecture 189 (status O): For a simple connected graph G, if max_v distEven(v) ≤ 1 + σ(G), then G has a Hamiltonian path. Here distEven(v) is the number of vertices at even distance from v, and σ(G) is the second-smallest degree of G's degree sequence (per WOWII defEntry 65).
WOWII Conjecture 19 If G is connected then the size b(G) of a largest induced bipartite subgraph satisfies b(G) ≥ FLOOR((∑ ecc(v))/(|V|) + sSup (range (l G))), where ecc(v) denotes eccentricity and l(G) is the independence number of neighbourhoods.
WOWII Conjecture 198a For a simple connected graph G, if b(G) ≤ 2 + ecc_avg(G), then G has a Hamiltonian path. Here b(G) is the number of vertices in a largest induced bipartite subgraph, and ecc_avg(G) is the average eccentricity of G.
WOWII Conjecture 199 For a simple connected graph G, if tree(G) - 2 ≤ κ(G), then G has a Hamiltonian path. The nontrivial vertex type encodes the source assumption n > 1. Here tree(G) is the number of vertices in a largest induced tree and κ(G) = vertexConnectivity G is the vertex connectivity of G.
WOWII Conjecture 40 For a nontrivial connected graph G the size f(G) of a largest induced forest satisfies f(G) ≥ ceil((p(G) + b(G) + 1)/2) where p(G) is the path cover number and b(G) is the largest induced bipartite subgraph size.
WOWII Conjecture 61 For a simple connected graph G, the size f(G) of a largest induced forest satisfies f(G) ≥ residue(G) + ⌈ diam(G) / 3 ⌉, where residue(G) is the Havel-Hakimi residue and diam(G) is the diameter of G.
WOWII Conjecture 72 For a simple connected graph G, tree(G) ≥ ⌈ecc_avg(G) + max_v λ(v)/3⌉ where tree(G) is the number of vertices in a largest induced tree, ecc_avg(G) is the average eccentricity of G, and max_v l(v) = max_v indepNeighborsCard G v is the maximum over all vertices of the…
WOWII Conjecture 84 (status O): For a simple connected graph G with positive minimum degree, tree(G) ≥ 2 · rad(G) / δ(G), where tree(G) is the number of vertices in a largest induced subtree, rad(G) is the radius, and δ(G) = G.minDegree is the minimum degree.
WOWII Conjecture 96 For a simple connected graph G on at least two vertices, α(G) ≤ 1 + min_v distEven(v) · (max_v l(v) - 1) where α(G) = G.indepNum is the independence number, distEven(v) is the number of vertices at even distance from v, and max_v l(v) is the maximum independence number of a…
Zagier's conjecture The ℚ-dimension of the vector space spanned by all multiple zeta values of weight n equals d_n, where d_n is the Zagier dimension sequence satisfying d_0 = 1, d_1 = 0, d_2 = 1, and d_n = d_n-2 + d_n-3 for n ≥ 3.
The Zariski Cancellation Problem: every polynomial ring over a field k of characteristic 0 is cancellative.
