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
A number $k$ is refactorable if its number of divisors, $\tau(k)$, divides $k$. Simon Colton conjectures that the number of refactorable numbers less than $x$ is at least $\frac{x}{2\log x}$. This is an asymptotic claim, so we state it for sufficiently large $x$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a74
Probably there is no such $A$ for the polynomial $X^3$. 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. Sou
I conjecture that { $a(n)$ ; $n>1$ } are the numbers such that $n^4-1$ divides $2^n-1$, intersection of A247219 and A247165. - M. F. Hasler, Jul 25 2015 This formalizes the reverse direction. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop
Let `V(x)` count the number of `n≤x` such that `ϕ(m)=n` is solvable. Does `V(2x)/V(x)→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 v
$a(n)$ = greatest prime of the form $k(n-k)-1$, or $0$ if no such prime exists. Conjecture: $a(n) > 0$ for $n > 3$. 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
When $A =\{a_1 < \cdots\}$ corresponds to the set of primes, it is conjectured that the $\limsup$ of the number of representations $$n=\sum_{u\leq i\leq v}a_i$$ is infinite. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definition is sup
$a(1) = 2$; $a(2n)$ = lcm of all previous terms + 1; $a(2n+1)$ = lcm of all previous terms - 1. Conjecture: There are infinitely many primes in this sequence. 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 p
Probably $f(x) = x^5$ has the property that the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct. 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
Let $a_1< a_2 < ⋯ $ be an infinite sequence of integers such that $a_1=1$ and $a_{i+1}$ is the least integer which is not a sum of consecutive earlier $a_j$s. Show that $a_k / k \to \infty$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop
$a(n)$ = number of primes of the form $k(n-k)-1$. Conjecture: $a(n) > 0$ for $n > 3$. 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 verifi
Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. Is $f(n)=o(n)$? Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definiti
Conjecture: $\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right) = A005156(n+1)/A005156(n)$ It is conjectured that $\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right) = A005156(n+1)/A005156(n)$, where the OEIS comment reads A005156 as 1-based; with the 0-indexed `b` this is `frac (n + 1) = b (n + 1) / b n`. Mathematical status Open: marked `research open` in google-deepmind/form
$a(1) = 393$; for $n > 1$, $a(n) = a(n-1)$ + 1 + sum of distinct prime factors of $a(n-1)$ that are $< a(n-1)$. Cormier and Selfridge found 5 starting values for which the sequences appear to not merge. The sequences were checked up to 10^8. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda
More generally, Bose and Chowla [BoCh62] conjectured that the maximum size of $A\subseteq \{1,\ldots,N\}$ with all $r$-fold sums distinct (aside from the trivial coincidences) then $\lvert A\rvert \sim N^{1/r}.$ Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal
Array read by upward antidiagonals: row $n$ ($n \ge 0$) contains the numbers $m^2 - n^2$, $m \ge n+1$. A "Goldbach Conjecture" for this sequence: when there are $n$ terms between consecutive odd integers $2n+1$ and $2n+3$ for $n > 0$, at least one will be the product of 2 primes (not necessarily distinct). Example: $n=3$ for consecutive odd integers $a(7) = 7$ and $a(11) = 9$ a
In [Er79] Erdős says perhaps $s_{n+1} - s_n \ll \log s_n$, but he is 'very doubtful'. [Er79] Erdős, Paul, __Some unconventional problems in number theory__. Math. Mag. (1979), 67-70. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop definiti
$a(n) = \sum_{k = n}^{2n} p_k$, where $p_k$ is the $k$-th prime. Terms are squares at only(?) three values of $n = 3, 6, 4072$: corresponding terms are 6^2, 13^2, and 15735^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 s
Let $a_1 < a_2 < \dots$ be a sequence of integers such that $\lim_{n\to\infty} \frac{a_n}{a_{n-1}^2} = 1$ and $\sum \frac{1}{a_n} \in \mathbb{Q}$. Then, for all sufficiently large $n \ge 1$, $a_n = a_{n-1}^2 - a_{n-1} + 1$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09
Conjecture from N. J. A. Sloane: $a(n) > 0$ for $n > 15$. 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. S
Let $f(n)$ count the number of solutions to $n=p+2^k$ for prime $p$ and $k\geq 0$. Show that $f(n)=o(\log 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 accept