Deciding hard small Turing machines (Busy Beaver)
Prove halting or non-halting of specific small Turing machines that current deciders cannot resolve.
0claims
0verified
Open problems in computability
Busy beaver values and other questions at the edge of what can be computed, where exhaustive, reproducible computation and formal proofs work together.
The Černý conjecture on synchronizing automata
Prove that every synchronizing complete DFA with n states has a reset word of length at most (n−1)². The best general upper bound is about 0.1654·n³ (Shitov 2019). The conjecture has been verified by computer for small automata.
0claims
0verified
Smallest n for which the value of BB(n) is undecidable
C_14 is the smallest n, such that the value of the busy beaver number BB(n) is undecidable in ZFC (or equivalently ZF). Explicitly, it is the smallest n such that there is a Turing machine with n states for which it cannot be proven in ZFC (assuming ZFC is consistent) whether it halts or not.
0claims
0verified
How to contribute in computability
- 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