Sums of a cube, a square, and a… to Characterization of Carmichael…
TheoremSums of a cube, a square, and a positive triangular number#
Number of ordered ways to write \(n\) as \(x^3 + y^2 + \frac{z(z+1)}{2}\) with \(x \ge 0\), \(y \ge 0\), and \(z > 0\).
References: - A262813
Quoted from FormalConjectures/OEIS/262813.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 2 open. It also has 5 test statements, counted here but not shown.
OeisA262813.conjecture_1
Open: stated without proof.
Conjecture: \(a(n) > 0\) for all \(n > 0\).
theorem conjecture_1 (n : ℕ) (hn : 0 < n) : 0 < a n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262813.lean, line 67.
OeisA262813.conjecture_2
Open: stated without proof.
Conjecture: \(a(n) = 1\) only for \(n = 1, 9, 21, 35, 98, 152, 306\).
theorem conjecture_2 (n : ℕ) (hn : 0 < n) :
a n = 1 ↔ n ∈ singletons
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262813.lean, line 74.
Sources
TheoremSums of a square and three weighted cubes#
Number of ordered ways to write \(n\) as \(w^2 + x^3 + 2y^3 + 3z^3\), where \(w, x, y\) and \(z\) are nonnegative integers.
References: - A262824
Quoted from FormalConjectures/OEIS/262824.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 5 research or textbook statements: 5 open. It also has 5 test statements, counted here but not shown.
OeisA262824.conjecture_1
Open: stated without proof.
Conjecture (i): For any \(m \in \{3, 4, 5, 6\}\) and \(n \ge 0\), there are nonnegative integers \(w, x, y, z\) such that \(n = w^2 + x^3 + 2y^3 + mz^3\).
theorem conjecture_1 (m : ℕ) (hm : m ∈ ({3, 4, 5, 6} : Finset ℕ)) (n : ℕ) :
∃ w x y z : ℕ, n = w ^ 2 + x ^ 3 + 2 * y ^ 3 + m * z ^ 3
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262824.lean, line 65.
OeisA262824.conjecture_2
Open: stated without proof.
Conjecture (ii): Every nonnegative integer \(n\) can be written as \(w^2 + x^3 + 2y^3 + z^4\) for some nonnegative integers \(w, x, y, z\).
theorem conjecture_2 (n : ℕ) :
∃ w x y z : ℕ, n = w ^ 2 + x ^ 3 + 2 * y ^ 3 + z ^ 4
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262824.lean, line 74.
OeisA262824.conjecture_3
Open: stated without proof.
Conjecture (ii): Every nonnegative integer \(n\) can be written as \(w^2 + x^3 + 2y^3 + 3z^4\) for some nonnegative integers \(w, x, y, z\).
theorem conjecture_3 (n : ℕ) :
∃ w x y z : ℕ, n = w ^ 2 + x ^ 3 + 2 * y ^ 3 + 3 * z ^ 4
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262824.lean, line 83.
OeisA262824.conjecture_4
Open: stated without proof.
Conjecture (ii): Every nonnegative integer \(n\) can be written as \(w^2 + x^3 + 2y^3 + 6z^4\) for some nonnegative integers \(w, x, y, z\).
theorem conjecture_4 (n : ℕ) :
∃ w x y z : ℕ, n = w ^ 2 + x ^ 3 + 2 * y ^ 3 + 6 * z ^ 4
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262824.lean, line 92.
OeisA262824.conjecture_5
Open: stated without proof.
Conjecture (ii): Every nonnegative integer \(n\) can be written as \(2w^2 + x^3 + 4y^3 + z^4\) for some nonnegative integers \(w, x, y, z\).
theorem conjecture_5 (n : ℕ) :
∃ w x y z : ℕ, n = 2 * w ^ 2 + x ^ 3 + 4 * y ^ 3 + z ^ 4
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262824.lean, line 101.
Sources
TheoremSums of a triangular number and three weighted cubes#
Number of ordered ways to write \(n\) as \(\frac{w(w+1)}{2} + x^3 + y^3 + 2z^3\) with \(w > 0\), \(0 \le x \le y\), and \(z \ge 0\).
References: - A262880
Quoted from FormalConjectures/OEIS/262880.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 2 open. It also has 5 test statements, counted here but not shown.
OeisA262880.conjecture_1
Open: stated without proof.
Conjecture (i): Any positive integer can be written as \(\frac{w(w+1)}{2} + x^3 + by^3 + cz^3\) with \(w > 0\) and \(x, y, z \ge 0\), provided that \((b, c) \in \{(1,2), (1,3), (1,4), (1,6), (2,2), (2,3), (2,4), (2,5), (2,6), (2,7), (2,20), (2,21), (2,34), (3,3), (3,4), (3,5), (3,6), (4,10)\}\).
theorem conjecture_1 (p : ℕ × ℕ) (hp : p ∈ pairs1) (n : ℕ) (hn : 0 < n) :
∃ w x y z : ℕ, 0 < w ∧ n = Nat.triangular w + x ^ 3 + p.1 * y ^ 3 + p.2 * z ^ 3
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262880.lean, line 74.
OeisA262880.conjecture_2
Open: stated without proof.
Conjecture (ii): For \((b, c) \in \{(3,4), (3,6), (4,8)\}\), every nonnegative integer \(n\) is of the form \(\frac{w(w+1)}{2} + 2x^3 + by^3 + cz^3\) for some nonnegative integers \(w, x, y, z\).
theorem conjecture_2 (p : ℕ × ℕ) (hp : p ∈ pairs2) (n : ℕ) :
∃ w x y z : ℕ, n = Nat.triangular w + 2 * x ^ 3 + p.1 * y ^ 3 + p.2 * z ^ 3
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/262880.lean, line 87.
Sources
TheoremRecurrence for Rule 167 cellular automaton sequence#
Decimal representation of the middle column of the "Rule 167" elementary cellular automaton starting with a single ON (black) cell.
References: - A267581 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/267581.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA267581.a_recurrence
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/267581.wip.lean#L190.
Conjecture: \(a(n) = 2 a(n-1) + 1 - \lfloor (1/2)^{2^{n+1} \bmod n} \rfloor\) for \(n \ge 2\). - Andres Cicuttin, Mar 29 2016
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem a_recurrence (n : ℕ) (hn : 2 ≤ n) : a n = 2 * a (n - 1) + 1 - oeisFloorTerm n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/267581.lean, line 105.
Sources
TheoremMaximal run lengths in the second MSB of Tribonacci numbers \(T(n)\)#
The Tribonacci numbers \(T_n\) (A000073). \(T_0=0, T_1=0, T_2=1\), and \(T_n = T_{n-1} + T_{n-2} + T_{n-3}\) for \(n \ge 3\).
Second most significant bit of the tribonacci number A000073(n). This is formalized by extracting the bit at position \(\lfloor \log_2 T_n \rfloor - 1\).
References: - A271591 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al. - A000073
Quoted from FormalConjectures/OEIS/271591.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA271591.maximal_run_lengths
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/271591.wip.lean#L497.
It is conjectured that after the first two 0's, the number of consecutive 0's is only 4 or 5, and the number of consecutive 1's is only 3 or 4 (tested up to \(n = 10^4\)).
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem maximal_run_lengths : (∀ n L, IsMaximalRun 0 n L → (L = 4 ∨ L = 5)) ∧
(∀ n L, IsMaximalRun 1 n L → (L = 3 ∨ L = 4))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/271591.lean, line 101.
Sources
TheoremCongruences \(a(n+k) \equiv a(n) \pmod k\) for hypergeometric values \({}_2F_1(n, -n; ; -1)\)#
a: \(a(n) = \text{hypergeometric}([n, -n], [], -1)\). This is equivalent to the combinatorial sum:
\[a(n) = \sum_{k=0}^n \binom{n}{k} \binom{n+k-1}{k} k!\]The expression uses \(\mathbb{N}\) arithmetic throughout, safely handling the subtraction via
Nat.pred.References: - A278070 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/278070.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA278070.a_modeq
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/278070.wip.lean#L68.
Conjecture: \(a(n+k) \equiv a(n) \pmod{k}\) for all \(n\) and \(k\). - Peter Bala, Mar 12 2023
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem a_modeq : ∀ (n k : ℕ), Nat.ModEq k (a (n + k)) (a n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/278070.lean, line 78.
Sources
TheoremThe 1680-Conjecture#
Any nonnegative integer can be written as \(x^2 + y^2 + z^2 + w^2\) with \(x, y, z, w\) nonnegative integers such that \(x^4 + 1680 y^3 z\) is a square.
Zhi-Wei Sun has offered a prize of 1,680 RMB for the first proof.
References: - A280831 - Z.-W. Sun, "Refining Lagrange's four-square theorem," J. Number Theory 175 (2017), 167-190. - Z.-W. Sun, "Refining Lagrange's four-square theorem," arXiv:1604.06723 [math.NT], 2016.
Quoted from FormalConjectures/OEIS/280831.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 7 test statements, counted here but not shown.
OeisA280831.conjecture
Open: stated without proof.
Zhi-Wei Sun's 1680-Conjecture (A280831): Any nonnegative integer can be written as \(x^2 + y^2 + z^2 + w^2\) with \(x, y, z, w\) nonnegative integers such that \(x^4 + 1680 y^3 z\) is a square.
theorem conjecture (n : ℕ) : A n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/280831.lean, line 76.
Sources
TheoremThe cup-of-coffee sequence#
The sequence starts with \(1, 2\). Each later term is the least unused positive integer such that, for every prime, runs of consecutive multiples have length exactly two. The local rule requires prime factors that have just appeared to occur once more, and forbids prime factors that occurred in both of the preceding terms.
References: - A280864
Quoted from FormalConjectures/OEIS/280864.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 15 test statements and 2 API statements, counted here but not shown.
OeisA280864.conjecture
Open: stated without proof.
Conjectured to be a permutation of the positive integers.
theorem conjecture :
∃ a : ℕ → ℕ, FollowsRule a ∧ ∀ k > 0, ∃ n, a n = k
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/280864.lean, line 238.
Sources
TheoremSum of four squares with square conditions#
Any integer \(n \geq 0\) can be written as \(x^2 + y^2 + z^2 + w^2\) with \(x, y, z, w\) nonnegative integers and \(z \leq w\), such that both \(x\) and \(x + 24y\) are squares.
Zhi-Wei Sun has offered a $2,400 prize for the first proof.
References: - A281976 - Z.-W. Sun, "Refining Lagrange's four-square theorem," J. Number Theory 175 (2017), 167-190. https://doi.org/10.1016/j.jnt.2016.11.008 - Z.-W. Sun, "Restricted sums of four squares," arXiv:1701.05868 [math.NT], 2017. https://arxiv.org/abs/1701.05868
Quoted from FormalConjectures/OEIS/281976.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 9 test statements, counted here but not shown.
OeisA281976.conjecture
Open: stated without proof.
Zhi-Wei Sun's Conjecture (A281976): Any integer \(n \geq 0\) can be written as \(x^2 + y^2 + z^2 + w^2\) with \(x, y, z, w\) nonnegative integers and \(z \leq w\), such that both \(x\) and \(x + 24y\) are squares.
theorem conjecture (n : ℕ) : A n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/281976.lean, line 86.
Sources
TheoremPeriod of \(p\)-th powers modulo \(n\)#
a: Period of cubes mod \(n\). The \(n\)-th term \(a(n)\) is the smallest positive integer \(T\) such that \(\forall k \in \mathbb{N}\), \((k+T)^3 \equiv k^3 \pmod n\).
The length of the minimal positive period of the sequence \(k^p \pmod n\). \(a_p(n) = \min \{ T \in \mathbb{N}^+ \mid \forall k \in \mathbb{N}, (k+T)^p \equiv k^p \pmod n \}\).
References: - A282779 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/282779.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA282779.periodOfPowerMod_eq
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/282779.wip.lean#L104.
Conjecture: let \(a_p(n)\) be the length of the period of the sequence \(k^p \bmod n\) where \(p\) is a prime, then \(a_p(n) = n/p\) if \(n \equiv 0 \pmod{p^2}\), else \(a_p(n) = n\).
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem periodOfPowerMod_eq (p n : ℕ) (hp : Nat.Prime p) (hn : n > 0) :
periodOfPowerMod p n = if p ^ 2 ∣ n then n / p else n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/282779.lean, line 73.
Sources
TheoremSum of a triangular number, a generalized pentagonal number, and a generalized heptagonal number#
Any nonnegative integer can be written as \(x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2\) with \(x, y, z\) nonnegative integers.
Zhi-Wei Sun offered a USD 135 prize for the first proof of this conjecture. Cao, Guo, Qiu, Feng and Gao proved it in [CGQFG26].
References: - A287616 - Zhi-Wei Sun, "Universal sums of three quadratic polynomials", arXiv:1502.03056 [math.NT] - [CGQFG26] Y. Cao, D. Guo, R. Qiu, R. Feng and X.-S. Gao, "Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number", arXiv:2606.26035
Quoted from FormalConjectures/OEIS/287616.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA287616.conjecture
Solved: stated here without proof.
Zhi-Wei Sun's Conjecture (A287616): Any nonnegative integer can be written as the sum of a triangular number \(x(x+1)/2\), a generalized pentagonal number \(y(3y+1)/2\), and a generalized heptagonal number \(z(5z+1)/2\), where \(x, y, z\) are nonnegative integers.
This was proved in [CGQFG26].
theorem conjecture (n : ℕ) : A n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/287616.lean, line 74.
Sources
TheoremSymmetry of digit sum differences \(\operatorname{sign}(S_5(k) - S_1(k))\)#
a: \(\mathrm{a}(n) = \sum_{k=0}^n \mathrm{sign}(\mathrm{A007953}(5k) - \mathrm{A007953}(k))\). \(\mathrm{A007953}(n)\) is the digital sum of \(n\) in base 10. The sequence is non-negative, so the sum over \(\mathbb{Z}\) is converted to \(\mathbb{N}\).
References: - A289411 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al. - A007953
Quoted from FormalConjectures/OEIS/289411.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA289411.a_symm
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/289411.wip.lean#L167.
Conjecture: For \(k \ge 1\), let \(m_k = 10^k / 2 - 1\). Then for \(i = 0, \ldots, m_k\), we have \(a(m_k - i) = a(m_k + i)\).
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem a_symm (k : ℕ) (hk : 0 < k) :
let m_k : ℕ := (10 ^ k) / 2 - 1
∀ i : ℕ, i ≤ m_k → a (m_k - i) = a (m_k + i)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/289411.lean, line 79.
Sources
TheoremStep difference bound \(a(n+1) - a(n) \in \{1, 2\}\) in mass-redistribution cellular automata#
\(a(n)\) is the number of steps needed to reach a stable configuration in the 1D cellular automaton initialized with one cell with mass \(n\) and based on the rule "each cell gives half of its mass, rounded down, to its right neighbor". The stable configuration is \(n\) cells with mass 1.
References: - A300997 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/300997.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA300997.a_succ_eq
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/300997.wip.lean#L1153.
Conjecture: It appears that the finite difference of this sequence only contains 1's and 2's.
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem a_succ_eq : ∀ n : ℕ, 1 ≤ n → a (n + 1) = a n + 1 ∨ a (n + 1) = a n + 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/300997.lean, line 149.
Sources
TheoremSum of two squares and two central-binomial-type terms#
A303639 counts the ways to write \(n\) as \(a^2 + b^2 + \binom{2c+1}{c} + \binom{2d+1}{d}\) with \(a, b, c, d\) nonnegative integers, \(a \le b\) and \(c \le d\).
References: - A303639 - Z.-W. Sun, "Restricted sums of four squares", arXiv:1701.05868 [math.NT], 2017-2018. - Z.-W. Sun, "Refining Lagrange's four-square theorem", J. Number Theory 175 (2017), 167-190. - S. Jeong, A303639 Counterexample Project, search, certificates and independent verifiers, DOI 10.5281/zenodo.21863025. The counterexample is recorded as an approved comment on the OEIS entry (Aug 10 2026).
Quoted from FormalConjectures/OEIS/303639.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 2 solved. It also has 6 test statements, counted here but not shown.
OeisA303639.conjecture
Solved: stated here; a Lean proof is at https://github.com/DCLXAI/a303639-counterexample/blob/8e21c57c622b05a1815bcf9927458ebb3973ef2e/lean/A303639/Counterexample.lean.
Zhi-Wei Sun's Conjecture (A303639): any integer \(n > 1\) can be written as \(a^2 + b^2 + \binom{2c+1}{c} + \binom{2d+1}{d}\) with \(a, b, c, d\) nonnegative integers. Sun checked this for \(n\) up to \(6 \cdot 10^8\).
This is false: \(n = 800322180\) admits no such representation, so \(a(800322180) = 0\). Since \(\binom{33}{16} > 800322180\), only \(c, d \le 15\) are possible, and each of the resulting \(136\) remainders \(800322180 - \binom{2c+1}{c} - \binom{2d+1}{d}\) is divisible by some prime \(p \equiv 3 \pmod 4\) to an odd power, hence is not a sum of two squares by Fermat's two-square theorem.
The counterexample is recorded as an approved comment on the OEIS entry; the Lean proof linked below formalises this argument, and was produced by Claude Opus 5 prompted by Sunsu Jeong (DCLXAI).
theorem conjecture : ¬ ∀ n : ℕ, 1 < n → A n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/303639.lean, line 96.
OeisA303639.conjecture.counterexample
Solved: stated here; a Lean proof is at https://github.com/DCLXAI/a303639-counterexample/blob/8e21c57c622b05a1815bcf9927458ebb3973ef2e/lean/A303639/Counterexample.lean.
The counterexample witnessing that A303639 vanishes: \(a(800322180) = 0\).
theorem conjecture.counterexample : ¬ A 800322180
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/303639.lean, line 103.
Sources
TheoremSum of two squares, a power of 3, and a power of 5#
Any integer \(n > 1\) can be written as \(a^2 + b^2 + 3^c + 5^d\) where \(a, b, c, d\) are nonnegative integers.
Zhi-Wei Sun has offered a $3,500 prize for the first proof.
References: - A303656 - Z.-W. Sun, "Restricted sums of four squares," arXiv preprint: https://arxiv.org/abs/1701.05868v10 - Z.-W. Sun, "Refining Lagrange's four-square theorem," Journal of Number Theory: http://maths.nju.edu.cn/~zwsun/RefineFourSquareTh.pdf - Z.-W. Sun, "Restricted sums of three or four squares": http://maths.nju.edu.cn/~zwsun/Square-sum.pdf - Zhi-Wei Sun's 1-3-5 conjecture and variations: https://www.aimspress.com/aimspress-data/era/2020/2/PDF/1935-9179_2020_2_589.pdf
Quoted from FormalConjectures/OEIS/303656.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 6 test statements, counted here but not shown.
OeisA303656.conjecture
Open: stated without proof.
Zhi-Wei Sun's Conjecture (A303656): Any integer \(n > 1\) can be written as the sum of two squares, a power of 3, and a power of 5.
theorem conjecture (n : ℕ) (hn : 1 < n) : A n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/303656.lean, line 77.
Sources
TheoremMaximality of \(k = 43\) with restricted digit counts in bases \(3 \le b < k\)#
Numbers \(k\) such that the base \(b\) expansion of \(k\) for each \(b = 3..k-1\) never contains more than two distinct digits.
The sequence Numbers \(k\) such that the base \(b\) expansion of \(k\) for each \(b = 3..k-1\) never contains more than two distinct digits.
References: - A306424 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/306424.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 12 test statements, counted here but not shown.
OeisA306424.forty_three_is_max
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/306424.wip.lean#L276.
Conjecture: The sequence is finite, with 43 being the last term.
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem forty_three_is_max : Condition 43 ∧ ∀ k : ℕ, 43 < k → ¬Condition k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/306424.lean, line 198.
Sources
TheoremThe 2-4-6-8 Conjecture#
Any integer \(n > 0\) can be written as \(\binom{w+2}{2} + \binom{x+3}{4} + \binom{y+5}{6} + \binom{z+7}{8}\) with \(w, x, y, z\) nonnegative integers.
Zhi-Wei Sun has offered a $2,468 prize for the first proof (or $2,468 RMB for a counterexample).
The conjecture has been verified for all \(n\) up to \(1.2 \times 10^{12}\) by Yaakov Baruch (March 2019).
The conjecture is false: \(n = 896315812331399\) has no such representation. The counterexample was found in the OEIS Open project, with a Lean proof.
References: - A306477 - mathoverflow/323541: Z.-W. Sun, "Positive integers written as C(w,2) + C(x,4) + C(y,6) + C(z,8) with w,x,y,z in {2,3,...},", Feb. 19, 2019. - T. Adamczewski, "OEIS Open: How many conjectures can language models turn into theorems?", arXiv:2608.11941 [cs.AI], 2026.
Quoted from FormalConjectures/OEIS/306477.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 6 test statements, counted here but not shown.
OeisA306477.conjecture
Solved: stated here; a Lean proof is at https://github.com/epoch-research/LeanOpenProblems-results/blob/fd09021e79869476ef83cda231312f1a2a89c8d7/runs/oeis-open-lite-fable51-wm0v421z5ygi8f6b/oeis_306477_conjecture_1/Submission/Spec.lean#L793.
Zhi-Wei Sun's 2-4-6-8 Conjecture (A306477): Any integer \(n > 0\) can be written as \(\binom{w+2}{2} + \binom{x+3}{4} + \binom{y+5}{6} + \binom{z+7}{8}\) for nonnegative integers \(w, x, y, z\).
This is false: \(n = 896315812331399\) is a counterexample. See T. Adamczewski, OEIS Open: How many conjectures can language models turn into theorems?, arXiv:2608.11941.
theorem conjecture : ¬ ∀ n : ℕ, 0 < n → A n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/306477.lean, line 84.
Sources
TheoremVanishing of bases with \(b^n \equiv -1 \pmod{2n+1}\) for absolute Euler pseudoprimes#
\(a(n)\) is the number of natural bases \(b < 2n+1\) such that \(b^n \equiv -1 \pmod{2n+1}\).
If \(2n+1\) is an absolute Euler pseudoprime, then \(a(n) = 0\).
References: - A307865 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
Quoted from FormalConjectures/OEIS/307865.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA307865.a_eq_zero_of_pseudoprime
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/307865.wip.lean#L190.
Conjecture: if \(2n+1\) is an absolute Euler pseudoprime, then \(a(n) = 0\).
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem a_eq_zero_of_pseudoprime (h : IsAbsoluteEulerPseudoprime (2 * n + 1)) : a n = 0
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/307865.lean, line 85.
Sources
TheoremFour-square conjecture with powers of 2, 3, and 5#
Any integer \(n > 1\) can be written as \((2^a \cdot 3^b)^2 + (2^c \cdot 5^d)^2 + x^2 + y^2\) where \(a, b, c, d, x, y\) are nonnegative integers.
Zhi-Wei Sun has offered a $2,500 prize for the first proof.
References: - A308734 - Z.-W. Sun, "Refining Lagrange's four-square theorem," J. Number Theory 175 (2017), 167-190. https://doi.org/10.1016/j.jnt.2016.11.008 - Z.-W. Sun, "Restricted sums of four squares," Int. J. Number Theory 15 (2019), 1863-1893. - Z.-W. Sun, "Various Refinements of Lagrange's Four-Square Theorem," Westlake Number Theory Symposium, Nanjing University, China, 2020. - S. Banerjee, "On a conjecture of Sun about sums of restricted squares," J. Number Theory 256 (2024), 253-289.
Quoted from FormalConjectures/OEIS/308734.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 5 test statements, counted here but not shown.
OeisA308734.conjecture
Open: stated without proof.
Zhi-Wei Sun's Four-Square Conjecture (A308734): Any integer \(n > 1\) can be written as \((2^a \cdot 3^b)^2 + (2^c \cdot 5^d)^2 + x^2 + y^2\) for nonnegative integers \(a, b, c, d, x, y\).
theorem conjecture (n : ℕ) (hn : 1 < n) : A n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/OEIS/308734.lean, line 73.
Sources
TheoremCharacterization of Carmichael numbers via squarefree denominators \(a(n)\)#
\(a(n)\) is the denominator of \(F(n) = \operatorname{num}(B_{n-1})/n + \operatorname{den}(B_{n-1})/n^2\).
A composite number \(n\) has squarefree \(a(n)\) if and only if \(n\) is a Carmichael number.
References: - A309132 - arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al. - A027641 - A027642
Quoted from FormalConjectures/OEIS/309132.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved. It also has 5 test statements, counted here but not shown.
OeisA309132.carmichael_iff_squarefree_a
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/309132.wip.lean#L353.
Conjecture: composite numbers \(n\) such that \(a(n)\) is squarefree are only the Carmichael numbers (A002997). - Thomas Ordowski, Jul 15 2019
A formal proof has been found with the methods described in arxiv/2605.22763.
theorem carmichael_iff_squarefree_a :
∀ (n : ℕ), (IsComposite n ∧ Squarefree (a n)) ↔ IsCarmichaelNumber n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/OEIS/309132.lean, line 86.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.