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
Erdős, Hardy, and Subbarao [HaSu02], believed that the number of $p \le x$ for which $f(p)=p−1$ is $o(x/\log x)$. [HaSu02] Hardy, G. E. and Subbarao, M. V., _A modified problem of Pillai and some related questions._ Amer. Math. Monthly (2002), 554--559. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f
Let $f(n;r,k)$ be the maximal number of edges in an $r$-uniform hypergraph which contains no set of $k$ many independent edges. For all $r\geq 3$, $$f(n;r,k)=\max\left(\binom{rk-1}{r}, \binom{n}{r}-\binom{n-k+1}{r}\right).$$ Note: the source states the formula with no range on `n` or `k`, but some restriction is needed: e.g. for `r = 3`, `k = 2`, `n = 4` no two disjoint triples
Granville and Soundararajan [GrSo98] have conjectured that at most $3$ powers of $2$ suffice for all odd integers, and hence at most $4$ powers of $2$ suffice for all even integers. Ref: Granville, A. and Soundararajan, K., _A Binary Additive Problem of Erdős and the Order of $2$ mod $p^2$_ Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures a
**Conjecture 1.3** (the $\times p, \times q$ conjecture): the only atomless Borel probability measure on $\mathbb{T}$ which is both $T_p$- and $T_q$-invariant is the Lebesgue measure. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definit
**Conjecture 1.1**: For any odd prime $k$, the sum associated with the classical theta function $θ_3$, $S(k)$ is positive. 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 mu
A Barker sequence is a finite sequence of $\pm 1$ values whose nontrivial aperiodic autocorrelations all have magnitude at most one. The Barker conjecture says that no such sequence has length greater than $13$. Every Barker sequence has length at most $13$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b238
For $n > 8$, $2^n$ is not the the sum of distinct powers of $3$. Expressed here in terms of the base $3$ digits of $n$. This conjecture is equivalent to the halting of a $15$-state $2$-symbol Turing Machine. TODO(lezeau): Formalize the Turing Machine version of this problem. Source: *Hardness of Busy Beaver Value BB(15)*: https://link.springer.com/chapter/10.1007/978-3-031-7262
For every integer n > 2, do there exist integers 1 ≤ x < y < z such that 4/n = 1/x + 1/y + 1/z? All fractions are rational numbers. This board asks for three distinct denominators; the more usual formulation permits repetitions and includes n = 2. Why it matters This asks how uniformly a simple rational number can be split into three unit fractions. Parametric identities cover
Is the real number e + π transcendental over the rational numbers? Here e = exp(1), and π is the usual circle constant. Transcendental means that no nonzero polynomial with rational coefficients has e + π as a root. This is stronger than asking whether e + π is irrational. Why it matters Knowing that e and π are individually transcendental says surprisingly little about their s
Let n ≥ 1 runners start together on a circle of circumference 1 and move with pairwise distinct constant real speeds, which may be negative. For each runner r, must there be a real time t ≥ 0 when its circular distance from every other runner is at least 1/n? Circular distance between positions x and y means min over integers m of |x−y−m|. The time may be different for differen
Let T be a finite tree, meaning a nonempty connected simple graph with no cycles, and let m be its number of edges. Can its vertices be given distinct integer labels from 0 through m so that the absolute differences of the labels at the ends of its edges are exactly 1, 2, …, m, each once? For a one-vertex tree, label its vertex 0; the required edge-difference list is empty. Why
For every integer t ≥ 1 and every finite simple graph G, if G cannot be coloured with t−1 colours so that adjacent vertices receive different colours, must G contain a K_t minor? Here a K_t minor means t nonempty, pairwise disjoint vertex sets, each inducing a connected graph, with an edge of G between every pair of sets. K_t is the complete graph on t vertices. Why it matters
Let G be a finite simple graph. Suppose every vertex has degree 3, its vertices can be split into two classes with every edge crossing between the classes, it can be drawn in the plane without crossing edges, and it is 3-connected: it has more than three vertices and stays connected after deleting any zero, one or two vertices. Must G have a cycle that visits every vertex exact
The sequence will eventually reach $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 provena
Is P = NP? A decision problem is a set of finite binary strings. P consists of problems decidable by a deterministic Turing machine in time bounded by a polynomial in the input length. NP consists of problems whose yes-instances have certificates of polynomially bounded length accepted by a deterministic polynomial-time verifier, with no accepted certificate for a no-instance.
For complex s with real part greater than 1, define ζ(s) = ∑ over integers n ≥ 1 of n^(−s), and extend it meromorphically to the complex plane. Does every zero s in the critical strip 0 < Re(s) < 1 satisfy Re(s) = 1/2? These are the nontrivial zeros; the known zeros at negative even integers are excluded. Why it matters The location of zeta zeros controls how the primes deviate