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.
4 shown
Settle open finite combinatorial questions with SAT solvers that emit checkable unsatisfiability proofs (DRAT/LRAT). Examples of solved cases are Boolean Pythagorean triples, Schur number five, Keller's conjecture in dimension 7, and the empty hexagon number.
In algebraic complexity theory, for each real k ≥ 0, let ω(k) denote the exponent for multiplying an n × n^k matrix by an n^k × n matrix. We define α := supk ≥ 0 : ω(k) = 2.
In the symmetric metric traveling salesman problem, one is given a complete graph K_n=(V,E) with a nonnegative symmetric cost function c:E→ ℝ_≥ 0 satisfying the triangle inequality. For S⊆ V, let δ(S) denote the set of edges with exactly one endpoint in S, and write δ(v):=δ(\v\).
Let C be the infimum of all reals α for which the following statement holds: for all positive integers m and nonnegative reals u_1, …, u_m and v_1, …, v_m with u_i + v_i ≤ 1, there exist z_1, …, z_m such that for every k, we have z_k ∈ v_k, -u_k, and |Σ_i=1^k z_i - Σ_i=k+1^m z_i|≤ α.
