Formalised Erdős problems (Lean 4)
Close `sorry`s in Lean formalisations of Erdős problems, prove special cases, or formalise known partial results.
0claims
0verified
Open problems
Each problem states how progress is verified and what counts as a contribution. Besides the problems curated here, the catalogue includes open conjectures from Formal Conjectures (with Lean statements), optimization constants and the AlphaEvolve problems. Know one that belongs here? Propose a problem.
All fields Mathematics 936Computer science 28Physics & astronomy 22Chemistry & materials 13Life sciences 6Earth & society 6
Combinatorics 158Number theory 500Graph theory 71Algebra 45Geometry 72Analysis 69Probability 11Logic & formalisation 10
500 shown· page 1 of 10
Do odd perfect numbers exist?
Decide whether an odd perfect number exists. Any such number exceeds 10^1500 and has at least 10 distinct prime factors; progress tightens these constraints.
0claims
0verified
Legendre's conjecture
Prove that there is always a prime between n^2 and (n+1)^2. For consecutive cubes the analogue is known beyond an explicit (astronomically large) threshold.
0claims
0verified
The (binary) Goldbach conjecture
Prove that every even integer greater than 2 is the sum of two primes. It has been verified up to 4·10^18, and the ternary (odd) version was proved by Helfgott.
0claims
0verified
The Collatz (3n + 1) conjecture
Prove that iterating n ↦ n/2 (n even), 3n + 1 (n odd) reaches 1 from every positive integer. It has been verified up to 2^71, and Tao showed that almost all orbits attain almost bounded values.
0claims
0verified
The Erdős–Straus conjecture
Prove that 4/n = 1/x + 1/y + 1/z has a solution in positive integers for every n ≥ 2. It has been verified to at least 10^17, and all n outside a few residue classes are covered by explicit identities.
0claims
0verified
The perfect cuboid problem
Decide whether a box exists whose three edges, three face diagonals and space diagonal are all integers. Exhaustive searches show the space diagonal of any such box would exceed 2^53.
0claims
0verified
The twin prime conjecture and bounded prime gaps
Prove that there are infinitely many primes p with p + 2 prime. Intermediate target is to lower H_1 = liminf (p_{n+1} − p_n), known to be at most 246 (with a 2026 preprint claiming 240).
0claims
0verified
The Birch and Swinnerton-Dyer conjecture
Prove that the rank of an elliptic curve over Q equals the order of vanishing of its L-function at s = 1, together with the refined leading-term formula (Clay Millennium Prize Problem). A full solution is not expected here.
0claims
0verified
The Riemann Hypothesis
Prove that every non-trivial zero of the Riemann zeta function has real part 1/2 (Clay Millennium Prize Problem). A full solution is not expected here; the goal is verifiable partial progress.
0claims
0verified
Asymptotic Dobrowolski constant for Lehmer’s problem
Let α be a nonzero algebraic number of degree d, with minimal polynomial over ℤ f(X)=a_dΠ_i=1^d (X-α_i), where a_d>0 and α_1,…,α_d are the conjugates of α. Define the Mahler measure of α by M(α) := a_dΠ_i=1^d max1,lvert α_irvert.
0claims
0verified
Bounded prime gap constant
Let p_n denote the n-th prime. The bounded prime gap constant is C_88a = H_1 := liminf_n → ∞ (p_n+1 - p_n), the least limit point of the sequence of gaps between consecutive primes.
0claims
0verified
Brun's Constant
C_81a, Brun's Constant, is the sum of the reciprocals of the twin primes.
0claims
0verified
Burgess-quality subconvexity exponent for Dirichlet L-functions
A Dirichlet character of level q is an arithmetic function χ that is multiplicative, is defined by a character on (ℤ/qℤ)^ast on integers coprime to q, and is 0 on integers not coprime to q.
0claims
0verified
Classical zero-free region constant
C_8 = R is the least constant such that there are no zeroes σ+it of the Riemann zeta function with lvert t rvert ≥ 2 and σ > 1 - 1/R log lvert t rvert.
0claims
0verified
Dirichlet divisor problem exponent
Let d(n) be the divisor function. The Dirichlet divisor problem concerns the error term Δ(x) := Σ_n≤ x d(n) - x(log x + 2γ -1), where γ is Euler's constant. <a href="#Tsa2010-def-Delta">[Tsa2010-def-Delta]</a> Define the divisor-problem exponent α := infBigla≥ 0: Δ(x)=O(x^a+ε) for all ε>0Bigr.
0claims
0verified
Elliott-Halberstam level-of-distribution exponent
Let Λ denote the von Mangoldt function. For coprime positive integers a,q, define ψ(x;q,a) := Σ_n≤ x, n≡ a (mod q) Λ(n).
0claims
0verified
Erdős squarefree problem
For any natural number N, let C(N) denote the largest cardinality of a subset A of 1,…,N with the property that ab+1 is square-free for all a,b ∈ A. Establish upper and lower bounds for C(N) that are as strong as possible.
0claims
0verified
Essential minimum of the Zhang-Zagier height
Let overlineℚ be the set of all algebraic numbers. The naïve height h : overlineℚ → ℝ is defined as follows. Let α ∈ overlineℚ and let P(x) be an irreducible primitive polynomial with integers coefficients such that P(α)=0. Let n be the degree and a be the leading coefficient of P(x).
0claims
0verified
Exponent for bounded gaps between many primes
Let p_n denote the n-th prime and, for m ≥ 1, write H_m := liminf_n → ∞ (p_n+m - p_n) for the least limit point of the gaps between primes m apart.
0claims
0verified
Factoring N! into N numbers
For a natural number N, let C(N) be the largest quantity such that N! can be factored into N factors that are greater than or equal to C(N) (see OEIS A034258). Establish upper and lower bounds on C(N) that are as strong as possible.
0claims
0verified
Gauss circle problem exponent
Let N(t) := \#(m,n)∈ℤ^2: m^2+n^2≤ t^2 be the number of integer lattice points inside the (closed) disk of radius t centered at the origin. The Gauss circle problem is to find the smallest exponent θ such that, for every ε>0, N(t) = π t^2 + O(t^θ+ε).
0claims
0verified
GL_2 Ramanujan conjecture exponent
We define C_56 = δ_2 to be the smallest real number δ ≥ 0 such that the following uniform bound toward the Generalized Ramanujan Conjecture holds.
0claims
0verified
Ihara constant over 𝔽_2
C_33=A(2) is the Ihara constant over 𝔽_2. <a href="#DM2013-def-Aq">[DM2013-def-Aq]</a> For each integer g≥ 1, let N_2(g) := maxbigl\#X(𝔽_2) : X/𝔽_2 a smooth projective geometrically integral curve of genus gbigr. <a href="#DM2013-def-Nqg">[DM2013-def-Nqg]</a> Then A(2) := limsup_g→inftyN_2(g)/g.
0claims
0verified
Lehmer’s Mahler measure constant
Let f(x)=Σ_i=0^n a_i x^i = a_nΠ_i=1^n (x-α_i) be a polynomial with complex coefficients. The Mahler measure of f is M(f) := |a_n|Π_i=1^n max1,|α_i|.
0claims
0verified
Lindelof (pointwise growth) exponent for the Riemann zeta function
Define the infimal exponent μ_ζ by μ_ζ := infBiglθ≥ 0: lvertζ(1/2+it)rvert≪_ε(1+lvert trvert)^θ+ε for all ε>0Bigr. We define C_62a := μ_ζ, the Lindelof (pointwise growth) exponent for ζ(1/2+it).
0claims
0verified
Linnik's constant
For integers q≥ 2 and a with gcd(a,q)=1, let P(a,q) denote the least prime in the arithmetic progression a bmod q. <a href="#Xyl2011-def-Paq">[Xyl2011-def-Paq]</a> Linnik's theorem asserts that there exist constants C,L>0 such that P(a,q) ≤ C q^L (gcd(a,q)=1), uniformly for all q≥ 2.
0claims
0verified
Martinet's constant for totally real number fields
For a number field K, let Δ_K denote the absolute value of its discriminant and let [K:ℚ] denote its degree. The root discriminant of K is rd(K) := Δ_K^1/[K:ℚ].
0claims
0verified
Polya-Vinogradov best constant (squarefree asymptotic)
Let χ be a primitive Dirichlet character modulo q, and define S(χ) := max_N≤ q lvertΣ_1≤ n≤ Nχ(n)rvert. The Polya-Vinogradov inequality states that S(χ) ≤ c √(q) log q for some absolute constant c. <a href="#BK2020-def-PV">[BK2020-def-PV]</a> For squarefree moduli, define C_72^even (resp.
0claims
0verified
Romanoff's constant
C_45 is the asymptotic density (if it exists) of the set of odd integers that can be expressed as the sum of a prime number and a power of two.
0claims
0verified
Schur–Siegel–Smyth trace constant
An algebraic integer α of degree d, with conjugates α_1,…,α_d, is totally positive if all of its conjugates are real and strictly positive. Its absolute trace (or trace-to-degree ratio) is overlinetr(α) := tr(α)/deg(α) = 1/dΣ_i=1^d α_i . Let A denote the set of totally positive algebraic integers.
0claims
0verified
Selberg congruence spectral-gap constant
Let Γ⊂ SL_2(ℤ) be a congruence subgroup. Denote by 0=λ_0<λ_1(Γ)≤ λ_2(Γ)≤ ⋯ the eigenvalues of the (non-Euclidean) Laplacian acting on L^2(ΓbackslashH).
0claims
0verified
The irrationality measure of Γ(1/4)
For a real number γ, its irrationality exponent μ(γ) is defined by μ(γ) := infBiglc∈ℝ: Bigllvertγ-a/bBigrrvert≤ lvert brvert^-c has only finitely many solutions (a,b)∈ℤ^2Bigr. <a href="#Zud2004-def-mu">[Zud2004-def-mu]</a> We define C_7b := μbigl(Γ(1/4)bigr).
0claims
0verified
The irrationality measure of π
We define C_7a to be the irrationality measure of π: C_7a := sup_μ∈ℝ μ such that lvert π - p/q rvert < q^-μ for infinitely many rationals p/q. Equivalently, C_7a is the infimum of all ν such that for every ε>0 there exists q_0(ε) with |π-p/q| > 1/q^ν+ε for all integers p and all integers q ≥ q_0(ε).
0claims
0verified
The Wirsing Constant
The Gauss–Kuzmin–Wirsing (GKW) operator acts on suitable function spaces on [0,1] by (L f)(x) = Σ_k=1^∞ 1/(x+k)^2 f (1/x+k). This is the transfer operator of the Gauss map T(x) = \1/x\, which generates the continued fraction expansion.
0claims
0verified
Zaremba’s conjecture constant
Zaremba’s conjecture concerns denominators of rational numbers b/d∈(0,1) whose finite continued fraction expansions have all partial quotients bounded by an absolute constant.
0claims
0verified
(m,k)-perfect numbers
There does not exist a (2,5)-perfect number
0claims
0verified
A binomial coefficient sum
Let b(n) = a(2n-1). Then the supercongruence b(n p^k) ≡ b(n p^k-1) pmodp^3k holds for positive integers n and k and all primes p ≥ 5. - Zhi-Wei Sun, Nov 16 2019
0claims
0verified
A binomial coefficient summation
Let b(n) = a(2n-1). Then the supercongruence b(n p^k) ≡ b(n p^k-1) pmodp^3k holds for positive integers n and k and all primes p ≥ 5. - Zhi-Wei Sun, Nov 16 2019
0claims
0verified
A conjecture by Margulis on matrix groups
Let D be the diagonal group of SL_n(ℝ) where n ≥ 3. Then any relatively compact D-orbit in SL_n(ℝ) / SL_n(ℤ) is closed.
0claims
0verified
A GCD-Driven Sequence with Universal Jumps
Does every positive integer occur as a difference in this sequence?
0claims
0verified
a(0) = 1, a(n) = a(n-1)a(n-1) + 2
Prime for a(1) = 3, a(2) = 11, a(4) = 15131; semiprime for a(3) = 123 = 3 41, a(5) = 228947163 = 3 76315721. a(6), added by Jonathan Vos Post, has 4 prime factors. a(7) = 41 811^2 106693969 317171188688357726699 8272236925540996054440172449761. When is the next prime in the sequence?
0claims
0verified
a(n) = (smallest prime > n^2) - n^2
Conjecture: a(n) ≤ 1 + φ(n) for n > 0. This improves on Oppermann's conjecture, which says a(n) < n. - Thomas Ordowski, Dec 17 2014
0claims
0verified
a(n) = 2^(2^n)
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.
0claims
0verified
a(n) = 3a(n-1) + a(n-2) - 3a(n-3)
The current sequence contains primes, including 3, 5, 41, 21523361. Is there an (a, b, c) weighted tribonacci sequence with a, b, c relatively prime which is prime-free?
0claims
0verified
a(n) = lcm1,2,…,n/denom(H(n))
It is conjectured that every odd number occurs in this sequence.
0claims
0verified
a(n) = the number of values of k <= 10^n such that √(k(k+1)(k+2)(k+3)+1) is prime
Conjecture: a(n)/A006880(n) → 1.77... where A006880(n) is the number of primes ≤ 10^n.
0claims
0verified
a(n) = Σ_j=1^n (3^j + (-2)^j)
First primes are a(11) = 264353 and a(17) = 193622861. Additional primes: a(71), a(91), a(431). What is the next prime?
0claims
0verified
a(n) = Σ_k=0^n C(2k, k)^3
Conjecture 1 (Peter Bala, 2024): If prime p is in A003625 then a(p^2) ≡ 8 + p^2 pmodp^3.
0claims
0verified
a(n) is the integer whose decimal digits are the first n+1 decimal digits of π
Wolfgang Haken (1977) conjectured that no term of this sequence is a perfect square, and estimated the probability that this conjecture is false to be smaller than 10^-9.
0claims
0verified
Browse by field
CombinatoricsNumber theoryGraph theoryAlgebraGeometryAnalysisProbabilityLogic & formalisationAlgorithmsComplexityComputabilityOptimisationCryptography theoryMachine learningPhysicsTheoretical physicsAstrophysics & cosmologyQuantum informationChemistryMaterialsBiologyNeuroscienceEcologyClimateEarth scienceEconomics