Browse the full public Ledger by latest public activity: problem creation, visible discussion posts and replies, or accepted submission updates.
Private jobs, votes, and description edits do not bump a problem. New activity can move problems between pages. This is one page of the Ledger, not the entire collection.
Browse all problems · Curated starting points
**Babai–Seress Conjecture (Conjecture 1.5)**: There exists an absolute constant $C$ such that the diameter of the alternating group $A_n$ satisfies $$\operatorname{diam}(A_n) \leq n^C.$$ *Reference:* [L. Babai and Á. Seress, *On the diameter of permutation groups*, European Journal of Combinatorics 13 (1992), Conjecture 1.5](https://doi.org/10.1016/S0195-6698(05)80029-0) Mathem
A factorial prime is a prime that is one more or one less than a factorial. It is conjectured that there are infinitely many factorial primes. There are infinitely many factorial primes. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop defi
There are no distinct primes $p$ and $q$ such that $\frac{q^p - 1}{q - 1}$ divides $\frac{p^q - 1}{p - 1}$ Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted b
A natural number $n$ is called a congruent number if there exists a right triangle with rational sides $a$, $b$, and hypotenuse $c$ such that the area of the triangle is $\frac{1}{2}ab = n$. Tunnell's theorem (sufficient condition assuming BSD) for odd squarefree congruent numbers. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revisio
Brennan's conjecture, part 1: $B(-2) = 1$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available. Sources and prov
Does the determinant of the sum $A + B$ of two $n \times n$ normal complex matrices $A$ and $B$ always lie in the convex hull of the $n!$ points $\prod\_i (\lambda(A)\_i + \lambda(B)\_{\sigma(i)})$? Here the numbers $\lambda(A)\_i$ and $\lambda(B)\_i$ are the eigenvalues of $A$ and $B$, and $\sigma$ is an element of the symmetric group $S\_n$. Mathematical status Open: marked `
There are infinitely many Fibonacci primes, i.e., Fibonacci numbers that are prime It is also a barrier to defining a benchmark from this paper: https://arxiv.org/html/2505.13938v1 (see Figure 8). Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A
Discrepancy of bounded-degree set systems. Given sets $S_1, \dots, S_m \subseteq [n]$ such that every element of $[n]$ belongs to at most $t$ of the sets (the system has *degree* at most $t$), one seeks a colouring $\chi \colon [n] \to \{-1, +1\}$ making every set as balanced as possible, i.e. minimizing the *discrepancy* $\max_i \left|\sum_{j \in S_i} \chi(j)\right|$. The Beck
**Rudin's conjecture.** The maximal number of squares among the first $N$ terms of a non-trivial arithmetic progression grows at most like $\sqrt{N}$: $$Q(N) = O(\sqrt{N}).$$ Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is su
A **Diophantine $m$-tuple** is a set of $m$ distinct positive integers $\{a_1, \dots, a_m\}$ such that $a_i a_j + 1$ is a perfect square for every $i \neq j$. The "strong Diophantine 5-tuple conjecture", so-called because it implies the Diophantine 5-tuple theorem (see `noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall`). [Du] Mathematical status Open: marked `resear
Ahlfors and Grunsky also conjectured in [AG37] that this upper bound is the precise value of the Bloch constant. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be acce
**Brocard's Conjecture** For every `n ≥ 2`, between the squares of the `n`-th and `(n+1)`-th primes, there are at least four prime numbers. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is supplied for the pinned Lean 4.33.1 e
This file formalizes the notion of a weakly first countable topological space and some conjectures around those. Problem 3 in [Ar2013]: Give an example in ZFC of a weakly first- countable compact Hausdorff space which is not first countable. Note: [Ar2013] uses a blanket convention that all spaces are Tychonoff and "compact" means compact Hausdorff. Mathematical status Open: ma
Let G be a finite bridgeless graph. Does G admit a nowhere-zero 5-flow, i.e. an orientation of its edges together with an integer value f(e) on each edge with 0 < |f(e)| < 5 such that at every vertex the sum of the values on incoming edges equals the sum on outgoing edges? Why it matters Open Problem Garden rates the problem "Outstanding": for planar graphs it follows from flow
Given a complex polynomial $p$ of degree $d ≥ 2$ and a complex number $z$ there is a critical point $c$ of $p$, such that $|p(z)-p(c)|/|z-c| ≤ |p'(z)|$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is supplied for the pinned
It is conjectured that there are infinitely many Wolstenholme primes. *Reference:* [Wikipedia](https://en.wikipedia.org/wiki/Wolstenholme_prime#Expected_number_of_Wolstenholme_primes) Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definit
Every even number greater than 4208 is the sum of two twin primes. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is ava
For every positive real number `ε`, there exist only finitely many triples `(a, b, c)` of coprime positive integers, with `a + b = c`, such that `c > rad(abc)^(1+ε)` Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is supplied fo
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. There are infinitely many Wilson primes. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). F
For any tree $T$ with $n$ edges, the complete graph $K_{2n+1}$ decomposes into $2n+1$ edge-disjoint copies of $T$ via cyclic shifts of a single embedding. The $2n+1$ copies are $f_0, f_1, \dots, f_{2n}$ where $f_i(v) = f_0(v) + i$ for all vertices $v$ — each copy is obtained by adding $i \pmod{2n+1}$ to every vertex of the base copy. This is strictly stronger than `RingelConjec