cff-version: 1.2.0
message: If you use results from this problem page, please cite it as below.
title: "Cairn Commons — Lean formalisation of Busy Beaver deciders and results"
type: dataset
license: CC-BY-4.0
url: "https://cairn-commons.com/problems/bbchallenge-lean-proofs"
date-released: 2026-09-28
authors:
  - name: Cairn Commons contributors
keywords:
  - "logic"
  - "busy-beaver"
  - "lean"
  - "coq"
  - "formal-verification"
  - "turing-machines"
  - "deciders"