Formalisation itself: turning informal mathematics into Lean statements and proofs that the kernel checks, plus open questions in logic and foundations.
Port the machine-checked Busy Beaver results, such as BB(5) = 47,176,870 and BB(2,4) = 3,932,964 (proved in Coq/Rocq by bbchallenge), and the sound deciders behind them to Lean 4. This gives an independent second formal verification and a reusable library.
Determine the value of the Busy Beaver function at n = 6.
Let G be a graph with chromatic number aleph_1. Is it true that there is a colouring of the edges with aleph_1 many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours? A problem of Erdős, Galvin, and Hajnal.
Determine which countable ordinals β have the property that, if α = ω^β, then in any red/blue colouring of the edges of K_α there is either a red K_α or a blue K_3.
Erdős Problem 598: Let m be an infinite cardinal and κ be the successor cardinal of 2^aleph_0. Can one colour the countable subsets of m using κ many colours so that every X ⊆ m with |X| = κ contains subsets of all possible colours?
Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B? Formally: let α be any type, let (A_i)_i ∈ I be a family of countably infinite subsets of α such that for all i ≠ j, the intersection A_i ∩ A_j is finite and |A_i ∩ A_j| ≠ 1.
Let X be a set of cardinality aleph_ω and f be a function from the finite subsets of X to X such that f(A)not∈ A for all A. Must there exist an infinite Y⊆ X that is independent - that is, for all finite B⊂ Y we have f(B)not∈ Y?
Erdős Problem 70: Let c be the order type of the real numbers, let β be a countable ordinal, and let 2 ≤ n < ω. Is it true that c → (β, n)^3_2? Note: The cases n ≤ 3 are trivially true (compare omega_three), so the genuine content of the conjecture begins at n = 4.
Tarski's exponential function problem. Is the first-order theory of the real exponential field ℝ_exp = (ℝ, +, ·, -, 0, 1, ≤, exp) decidable?
The Vaught conjecture states that for a countable language L and a complete L-Theory T the number of countable models of T (up to isomorphism) is finite, aleph_0 or 2^aleph_0.
Everything is published under CC BY 4.0 with authorship recorded. How it works
