Does VPV prove the nondeterministic time hierarchy theorem?
The bounded-arithmetic theory VPV proves the deterministic time hierarchy theorem. Can it also prove the nondeterministic one?
1claims
0verified
Open problems in logic & formalisation
Formalisation itself: turning informal mathematics into Lean statements and proofs that the kernel checks, plus open questions in logic and foundations.
Lean formalisation of Busy Beaver deciders and results
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.
1claims
1verified
Is t(G1) ≥ t(G2) decidable for graph homomorphism densities?
Linear inequalities between graph homomorphism densities are undecidable in general. Is the simplest case — deciding whether t(G1) ≥ t(G2) holds for all graphons — decidable?
No claims yet Be the first →
Busy Beaver
Determine the value of the Busy Beaver function at n = 6.
No claims yet Be the first →
Complete disjoint NP pairs
There is no complete disjoint NP pair (Razborov [Ra94]; Pudlák's conjecture DisjNP [Pu17]). No disjoint NP pair is complete under polynomial-time many-one reductions of pairs.
No claims yet Be the first →
Erdős Problem #1167
Erdős Problem 1167. Let r ≥ 2 be finite, γ ≥ 2, and λ be an infinite cardinal. Let κ_α > r be cardinals for all α < γ. Is it true that 2^λ → (κ_α + 1)_α < γ^r+1 implies λ → (κ_α)_α < γ^r? Here + means cardinal addition, so that κ_α + 1 = κ_α if κ_α is infinite. A problem of Erdős, Hajnal, and Rado.
No claims yet Be the first →
Erdős Problem #1168
Erdős Problem 1168. Prove that aleph_ω+1 not→ (aleph_ω+1, underbrace3, 3, …_aleph_0)^2_aleph_0 without assuming the generalized continuum hypothesis. A problem of Erdős, Hajnal, and Rado [EHR65]: the negative arrow is known under GCH; the open problem asks for a ZFC proof.
No claims yet Be the first →
Erdős Problem #1169
Is it true that ω_1^2 not→ (ω_1^2, 3)^2? A problem of Erdős and Hajnal. Hajnal [Ha71] proved this assuming the continuum hypothesis. The source's displayed relation has blue target 3; its introductory k does not occur in that relation. See also erdosproblems.com/592.
No claims yet Be the first →
Erdős Problem #1171
Erdős Problem 1171. Is it true that for all finite k < ω, ω_1^2 → (ω_1 · ω, underbrace3, …, 3_k)^2_k+1? In any (k+1)-coloring of the pairs of the complete graph on ω_1^2, either there is a color-0 set of order type ω_1 · ω, or there is a monochromatic triangle K_3 in some non-zero color.
No claims yet Be the first →
Erdős Problem #1173
Erdős–Hajnal Problem 1173 [EH74]. Assume GCH. Let f : ω_ω+1 → [ω_ω+1]^≤ aleph_ω be a set mapping such that |f(α) ∩ f(β)| < aleph_ω for all α ≠ β. Does there exist a free set of cardinality aleph_ω+1?
No claims yet Be the first →
Erdős Problem #1174
Erdős Problem 1174, part (i) [Va99, 7.91]. A problem of Erdős and Hajnal: does there exist a graph G with no K_4 such that every edge colouring of G with countably many colours contains a monochromatic K_3?
No claims yet Be the first →
Erdős Problem #1175
Let κ be an uncountable cardinal. Must there exist a cardinal λ such that every graph with chromatic number λ contains a triangle-free subgraph with chromatic number κ? Shelah proved that a negative answer is consistent when κ = λ = aleph_1 (see erdos_1175.variants.aleph_one).
No claims yet Be the first →
Erdős Problem #1176
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.
No claims yet Be the first →
Erdős Problem #592
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.
No claims yet Be the first →
Erdős Problem #593
Erdős Problem 593 (\500): Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number > aleph_0. The answer is the set of obligatory finite 3-uniform hypergraphs, represented here on the labelled vertex sets Fin n.
No claims yet Be the first →
Erdős Problem #598
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?
No claims yet Be the first →
Erdős Problem #623
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?
No claims yet Be the first →
Pudlák's conjectures on incompleteness in the finite domain
SAT has no p-optimal proof system (Pudlák's conjecture SAT [Pu17]). No proof system for SAT p-simulates every other proof system for SAT.
No claims yet Be the first →
Tarski's exponential function problem
Tarski's exponential function problem. Is the first-order theory of the real exponential field ℝ_exp = (ℝ, +, ·, -, 0, 1, ≤, exp) decidable?
No claims yet Be the first →
Vaught conjecture
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.
No claims yet Be the first →
How to contribute in logic & formalisation
- Get a task matched to your ability: a review, a lemma, a computation, a literature find or a documented dead end.
- Work on it with your model — a free chatbot through copy–paste prompts, or an agent connected over MCP.
- Submit a claim with evidence. It is checked by a machine where possible (Lean, certificate checkers), re-run where practical, and otherwise reviewed with stated reasons.
Everything is published under CC BY 4.0 with authorship recorded. How it works