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.
The area of a regular $n$-gon with side length 1 is given by $\frac{n}{4} \cot(\pi / n) = \frac{n}{4 \tan(\pi / n)}$. "Usually (perhaps always?) $\lfloor n^2 / (4\pi) - \pi / 12 \rfloor$ for a polygon of circumference $n$. Note that the area of a circle with circumference $C$ is $C^2 / (4\pi)$." Mathematical status Open: marked `research open` in google-deepmind/formal-conjectu
There are infinitely many real quadratic fields `ℚ(√d)` with class number one, where `d > 1` is a squarefree 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
The sequence $a(n)$ satisfies $\sum_{k \mid n} \frac{a(k)}{k!} = \sum_{j=1}^n \frac{1}{j} = H_n$, where the sum on the left is over positive divisors $k$ of $n$. By Möbius inversion, $$a(n) = n! \sum_{d \mid n} \mu(n/d) H_d$$ where $H_d = \sum_{j=1}^d \frac{1}{j}$ is the $d$-th harmonic number. The terms are not all positive. The first negative one is $a(30) = -2269064464730281
A repunit is a number whose digits in some base are all $1$. Here a nontrivial representation has at least three digits. The Goormaghtigh conjecture says that $31$ and $8191$ are the only numbers having nontrivial repunit representations in two different bases. The only Goormaghtigh numbers are $31$ and $8191$. Mathematical status Open: marked `research open` in google-deepmind
The sequence $a(n)$ is the number of times the binary expansion of $n$ appears as a contiguous sublist (infix) in the binary expansion of $n^2$. Is $a(n) \le 1$ for all $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 sup
The Elliott–Halberstam conjecture: for every $\theta < 1$ and $A > 0$ there exists a constant $C > 0$ such that $$\sum_{1 \le q \le x^{\theta}} E(x; q) \le \frac{C x}{\log^A x}$$ for all $x > 2$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A
The sequence $a(n)$ gives the smallest $k$ such that the decimal expansion of $k!$ contains exactly $n$ occurrences of the digit '6', or $0$ if no such $k$ exists. It is conjectured that $a(24) = 0$ since no factorial less than $10000$ contained just 24 sixes. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2
The $n$-th term $a(n)$ is given by $$a(n) = \sum_{k=0}^{n-1} \frac{1}{k+1} \binom{2k}{k} \binom{k}{n-1-k}$$ Conjecture: for $n > 0$, $a(n)$ is also the number of sequences of length $n - 1$ covering an initial interval of positive integers and avoiding three terms $(\dots, x, \dots, y, \dots, z, \dots)$ such that $x \le y \le z$. - Gus Wiseman, Jun 17 2021 Mathematical status O
For positive integers $k$ and $m$, let $$S_k(m)=1^k+2^k+\cdots+(m-1)^k.$$ The Erdős–Moser conjecture says that $S_k(m)=m^k$ has only the solution $(k,m)=(1,3)$. The only positive solution of $S_k(m)=m^k$ is $(k,m)=(1,3)$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-1
The Catalan-Larcombe-French sequence defined by $a(0)=1$, $a(1)=8$, and $$n^2 a(n) = 8(3n^2 - 3n + 1) a(n-1) - 128(n-1)^2 a(n-2)$$ for $n \ge 2$. Conjecture: let $P(n)$ be the $(n+1) \times (n+1)$ Hankel-type determinant with $(i,j)$-entry equal to $a(i+j)$ for all $i,j = 0, \ldots, n$. Then $P(n)/2^{n(n+3)}$ is a positive odd integer. - Zhi-Wei Sun, Aug 14 2013 Mathematical st
The sequence $a(n)$ counts the number of integers $s \in \{1, \dots, n-1\}$ such that $n^2 + s^2$ is prime: $$a(n) = \sum_{s=1}^{n-1} [\text{Prime}(n^2 + s^2)]$$ Conjecture: $a(n) > 0$ for all $n > 1$. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availabil
A067720 lists numbers $k$ such that $\varphi(k^2 + 1) = k \cdot \varphi(k + 1)$, where $\varphi$ is Euler's totient function. The sequence exhibits a strong connection to primes: for almost all terms $k$, $k + 1$ is prime. The conjecture states that $k = 8$ is the only exception. For members of the sequence other than $8$, we have $k + 1$ is prime. Mathematical status Open: mar
**Büchi's problem (first open case, $M = 5$)**: For all integers $x$ and $a$, if $(x+n)^2 + a$ is a perfect square for $n = 0, 1, 2, 3, 4$, then $a = 0$. Non-trivial sequences of length 3 and 4 are known to exist, so $M = 5$ is the first open case. Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3
Number of primes strictly less than $n^2$. Conjecture: all the numbers $\sum_{i=j}^k \frac{1}{a(i)}$ with $1 < j \le k$ have pairwise distinct fractional parts. - Zhi-Wei Sun, Sep 24 2015 Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11). Formal availability A Prop def
For every positive natural number $n$, there exists a natural number $m$ with $m ≠ n$, such that $φ(n) = φ(m)$ where $φ$ is the Euler totient function. *Carmichael's totient function conjecture*: For every positive natural number $n$, there exists a natural number $m$ with $m ≠ n$, such that $φ(n) = φ(m)$. Mathematical status Open: marked `research open` in google-deepmind/form
The $n$-th prime number $p_n$, where $p_1 = 2$. **Conjecture from Thomas Ordowski (2023)**: $\log \log a(n+1) - \log \log a(n) < 1/n$ for $n > 0$. 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
The smallest positive integer $m$ whose Euler totient equals $n!$. Conjecture: unless $n! + 1$ is prime (i.e., $n \in \text{A002981}$), $a(n) = p q$ where $p$ is the least prime $> \sqrt{n!}$ such that $(p - 1) \mid n!$ and $q = \frac{n!}{p - 1} + 1$ is prime. - M. F. Hasler, Oct 04 2009 We assume $a(n) \ne 0$ and $(p(n)).\text{Prime}$ to ensure the `sInf` searches are non-empt
The difference between the smallest prime strictly greater than $n^2$ and $n^2$. Conjecture: $a(n) \le 1 + \phi(n)$ for $n > 0$. This improves on Oppermann's conjecture, which says $a(n) < n$. - Thomas Ordowski, Dec 17 2014 Mathematical status Open: marked `research open` in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09
The **Beal Conjecture**: if we are given positive integers $A, B, C, x, y, z$ such that $x, y, z > 2$ and $A^x + B^y = C^z$ then $A, B, C$ have a common divisor. 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 th
Agrawal's conjecture is a stronger version of the theorem that forms the basis of the AKS primality test. If true, it would significantly improve the efficiency of primality testing. The conjecture states that for coprime $n$ and $r$, if the polynomial congruence $(X-1)^n \equiv X^n-1 \pmod{n, X^r-1}$ holds, then $n$ is either prime or $n^2 \equiv 1 \pmod{r}$. **Roman B. Popovy