Skip to content
238 open problems · 238 with Lean statements · 1 being worked on · 1 verified results

Open conjectures from the OEIS

Conjectures stated in OEIS entries — that a sequence is infinite, that a formula holds for all n, that some search never ends — formalised in Lean by Formal Conjectures. Many can be tested by computing more terms, and a counterexample is a checkable certificate.

Source: The On-Line Encyclopedia of Integer Sequences. Licence: Lean statements from Formal Conjectures (Apache 2.0).

Level A · Machine-checkable Hard Number theory Lean statement

Smallest x such that σ(x) bmod x = n

At present, the 0 entry for n = 5 is only a conjecture. That is, it is conjectured that there is no positive integer x such that σ_1(x) bmod x = 5.

No claims yet Be the first →
Level A · Machine-checkable Hard Number theory Lean statement

Sum of four squares with square conditions

Zhi-Wei Sun's Conjecture (A281976): Any integer n ≥ 0 can be written as x^2 + y^2 + z^2 + w^2 with x, y, z, w nonnegative integers and z ≤ w, such that both x and x + 24y are squares.

No claims yet Be the first →
Level A · Machine-checkable Hard Number theory Lean statement

Sum of next n primes

The only positive integer n such that a(n) is a perfect square is n=38. - Carlos Eduardo Olivieri, Mar 09 2015

No claims yet Be the first →
Level A · Machine-checkable Hard Number theory Lean statement

Sum of squares of divisors of n

Conjecture: For each k = 2,3,..., all the rational numbers σ_k(n)/n^k = Σ_d|n 1/d^k (n = 1,2,3,...) have pairwise distinct fractional parts. - Zhi-Wei Sun, Oct 15 2015

No claims yet Be the first →
Level A · Machine-checkable Hard Number theory Lean statement

Sums of a triangular number and three weighted cubes

Conjecture (i): Any positive integer can be written as w(w+1)/2 + x^3 + by^3 + cz^3 with w > 0 and x, y, z ≥ 0, provided that (b, c) ∈ (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).

No claims yet Be the first →
Level A · Machine-checkable Hard Number theory Lean statement

The 1680-Conjecture

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.

No claims yet Be the first →
Level A · Machine-checkable Hard Number theory Lean statement

The prime numbers

Conjecture from Thomas Ordowski (2023): log log a(n+1) - log log a(n) < 1/n for n > 0.

No claims yet Be the first →
Level A · Machine-checkable Hard Number theory Lean statement

Wolstenholme numbers

Conjecture: for n > 3, gcd(n, a(n-1)) = A089026(n). - Amiram Eldar and Thomas Ordowski, Jul 28 2019

No claims yet Be the first →