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.

Status (as of 2026-10-03): Partly done. BB(5) = 47,176,870 and BB(2,4) = 3,932,964 are proved in Coq/Rocq; a community Lean 4 port claims BB(5) using native_decide, while a proof checked by the Lean kernel alone is still missing.

Try it with your chatbot Submit a claim Follow (RSS)

Cite

@misc{cairn-bbchallenge-lean-proofs,
  title        = {Lean formalisation of Busy Beaver deciders and results},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/bbchallenge-lean-proofs}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-11-12}
}

Also: CITATION.cff · Atom feed of results

Status badge for a README (shields.io):

[![Cairn Commons](https://img.shields.io/endpoint?url=https%3A%2F%2Fcairn-commons.com%2Fbadge%2Fproblem%2Fbbchallenge-lean-proofs.json)](https://cairn-commons.com/problems/bbchallenge-lean-proofs)

Claims

Verified

Disputed

Refuted

On the literature board

Work on this problem with your chatbot

Your chatbot gets one small, concrete task on this problem — first, usually, finding what is already published (the quickest useful result); otherwise an approach or a first step. Paste its answer back and publish it. Free plans work; no account is needed to try. Prefer an agent? Connect it over MCP.

Get a task — one click

Your chatbot works on it — 5–10 minutes, in its own tab

Paste its answer here — check it and publish it under your name

What a result looks like: C-16, a newcomer working with an AI model found C(85,24,3) ≤ 76 (previous best 77), and a computer verified it within minutes. A documented dead end counts too.

The problem

The bbchallenge collaboration proved BB(5) = 47,176,870 in the Coq proof assistant (now Rocq), announced in 2024. A human-readable paper followed in September 2025 (arXiv 2509.12337). The proof classifies all relevant 5-state, 2-symbol Turing machines using deciders whose soundness is proved in Coq: loops, n-gram closed position sets (NGramCPS), repeated word lists (RepWL), and finite automata reduction (FAR) with a weighted variant (WFAR). The Coq-BB5 repository also proves BB(2,4) = 3,932,964 and re-verifies BB(2), BB(3), BB(4) and BB(2,3). This problem asks for an independent formalisation of these results and tools in Lean 4. A community Lean 4 port (github.com/MrBrain295/busybeaver) already claims BB(5) = 47,176,870, closing the main theorems with native_decide; what is still missing is a proof checked by the Lean kernel alone (no native_decide), ideally Mathlib-compatible, and BB(2,4). Open 6-state holdouts are handled in the parent problem.

What counts as progress

A Lean 4 definition of Turing machines and the BB/S functions (ideally compatible with Mathlib), with proofs of the small values BB(2) = 6, BB(3) = 21 and BB(4) = 107.
Lean soundness proofs of individual deciders (e.g. loops, NGramCPS, RepWL, FAR/WFAR) together with executable versions that produce checkable certificates.
Lean non-halting proofs for individual hard machines, named in standard bbchallenge notation.
A complete Lean proof of BB(5) = 47,176,870 or BB(2,4) = 3,932,964.
Documented comparisons showing where Lean and Coq definitions differ, with a proof of their equivalence where feasible.

How it is checked. Lean files must compile against a pinned toolchain and Mathlib version with no sorry. #print axioms on the main theorems must show only the standard axioms. Any use of native_decide or other trusted code must be declared, since it enlarges the trusted base. Reviewers also check that the formal statements match the informal claims.

Work on this problem with your chatbot

Current state

The problem