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
Why do polynomials with coefficients 0,1 like to have only factors with 0,1 coefficients? Let $P(x), Q(x) ∈ ℝ[x]$ be two monic polynomials with non-negative coefficients. If $R(x) = P(x)Q(x)$ is a $0,1$ polynomial (coefficients only from $\{0,1\}$), then $P(x)$ and $Q(x)$ are also $0, 1$ polynomials. Mathematical status Open: marked `research open` in google-deepmind/formal-con
If $2^x$ and $3^x$ are integers, then $x$ must be an integer. 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 availabl
Let $f(n) = n + \text{sum of the digits of } n$. If $f(n)$ is multiple of $n$ then $a(n)= f(n)$ else $a(n) = f(f(f(n)))\dots$ until one gets a multiple of $n$; $a(n) = 0$ if no such number exists. A100800 Conjecture: No term is zero. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (check
Ecklund, Erdős, and Selfridge [EES74] conjectured $g(k)\leq \exp((1+o(1))k)$. 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 befor
More commonly known as the **no-three-in-line problem**. What is the largest subset of the grid $[N]^2$ with no three points in a line? In particular, for $N$ sufficiently large, is it impossible to have a set of size $2N$ with this property? The upper bound $2N$ is the easy half and is `allowedSetSize_le` below, by pigeonhole on the columns. The open content is whether $2N$ is
Are there only finitely many binomial coefficients with deficiency > 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 i
Is every odd $n > 1$ the sum of a squarefree number and a power of 2? 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
Prove that there exists some $c>0$ such that $$h(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}$$ as $n\to \infty$. 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 ac
For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$, with only finitely many exceptions. 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 a
It is likely that there are infinitely many primes $p$ such that $8p^2 - 1$ is also prime. 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 v
Weisenberg has observed that Dickson's conjecture implies the answer is no if we replace $p_1\cdots p_k$ with $p_1\cdots p_k-1$. Indeed, let $L_k$ be the lowest common multiple of all integers at most $p_1\cdots p_k$. By Dickson's conjecture [Wikipedia], there are infinitely many $n'$ such that $\frac{L_k}{m}n'+1$ is prime for all $1\leq m < p_1\cdots p_k$. It follows that, if
If $A\subseteq\{1, ..., N\}$ with $|A| = n$ is such that the subset sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$ then $$ N \gg 2 ^ 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 supplied for the pinned Lea
**Conjecture 1 (Fernandes, 2026):** Let $m \ge n \ge 2$ be integers with $(m, n) \notin \{(2,2), (3,3), (4,3), (4,4)\}$. Then the group $$ \Gamma_{m \oplus n} = \{(\sigma_1, \sigma_2) \in \mathrm{S}_m \times \mathrm{S}_n : \mathrm{sgn}(\sigma_1) = \mathrm{sgn}(\sigma_2)\} $$ has rank $2$, i.e., minimal generating set of size $2$. Note: Fernandes states the conjecture for groups
Problem 10.6. Find a very rapidly increasing sequence $(m_n)_{n \ge 1}$ of positive integers such that $(\{\xi m_n\})_{n \ge 1}$ is dense modulo one for every irrational number $\xi$. Note: Furstenberg's $2^m3^n$ is sublacunary but requires two parameters. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f
Let $v(n,k)$ count the prime factors of $n+k$ which do not divide $n+i$ for $0\leq i < k$. Is it true that $v_0(n)=\max_{k\geq 0}v(n,k)\to \infty$ as $n\to \infty$? 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
It is probably true that `h n = 3` for infinitely many `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 supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
A Conjecture of Marian Deaconescu, see p.120 in https://doi.org/10.2307/2975810 [Needed to index shift in order to avoid trivial case $n = 0$, where the conjecture is trivially false.] Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop defini
Let $G$ be a graph with chromatic number $k$ containing no $K_k$. If $a,b\geq 2$ and $a+b=k+1$ then must there exist two disjoint subgraphs of $G$ with chromatic numbers $\geq a$ and $\geq b$ respectively? Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal avail
Atiyah and Sutcliffe associate a homogeneous binary polynomial to each point in a configuration of distinct points in Euclidean three-space. Their first conjecture says that these polynomials are always linearly independent. [Atiyah–Sutcliffe Conjecture 1](https://doi.org/10.1098/rspa.2001.0913), stated as Conjecture 1.1 in [Mazur–Petrenko](https://arxiv.org/abs/1102.4662): the
This file contains the formalisation of [GoLo21] up to and including Conjecture 1.8. $F(n) \leq n^{3/2}$. 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