1 of 51

Coq proof of the 5th Busy Beaver value

Tristan Stérin, The bbchallenge Collaboration�bbchallenge.org

ERC No 772766, SFI 18/ERCS/5746

2 of 51

Does it halt?

Step #0

3 of 51

Does it halt?

Step #1

4 of 51

Does it halt?

Step #2

5 of 51

Does it halt?

Step #3

6 of 51

Does it halt?

Step #4

7 of 51

Does it halt?

Step #5

8 of 51

Does it halt?

Step #6

9 of 51

Does it halt?

Will we ever read a 0 in state E ?

Step #6

10 of 51

Does it halt?

Will we ever read a 0 in state E ?

Step #6

11 of 51

Does it halt?�Yes!

The machine has halted!!

Step #47,176,870

12 of 51

Does it halt?�Yes!

20,000-step space-time diagram

Each row is a successive tape
White = 1, Black = 0

13 of 51

Does it halt?

The machine has halted!!

Can another 5-state machine do better?

Step #47,176,870

14 of 51

The Busy Beaver function

BB(n) = “Maximum number of steps done by a halting 2-symbol Turing machine with n states starting from all-0 memory tape”

T. Radó. On Non-computable Functions. Bell System Technical Journal, 41(3):877–884. 1962.

Tibor Radó, 1895 - 1965

BB(n) = “Maximum algorithmic bang for your buck”

UNCOMPUTABLE

15 of 51

The Busy Beaver function

BB(n) = “Maximum number of steps done by a halting 2-symbol Turing machine with n states starting from all-0 memory tape”

T. Radó. On Non-computable Functions. Bell System Technical Journal, 41(3):877–884. 1962.

Allen Brady, 1934 - 2024

BB(1) = 1, BB(2) = 6 [Radó, 1962]
BB(3) = 21 [Radó and Lin, 1963]
BB(4) = 107 [Brady, 1983]

Small busy beaver values:

A 4-state Turing machine that runs more than 107 steps never halts (from all-0 tape)

16 of 51

The Busy Beaver function

BB(n) = “Maximum number of steps done by a halting 2-symbol Turing machine with n states starting from all-0 memory tape”

T. Radó. On Non-computable Functions. Bell System Technical Journal, 41(3):877–884. 1962.

BB(1) = 1, BB(2) = 6 [Radó, 1962]
BB(3) = 21 [Radó and Lin, 1963]
BB(4) = 107 [Brady, 1983]
BB(5) ≥ 47,176,870 [Marxen and Buntrock, 1989]

Small busy beaver values:

BB(5) = 47,176,870?

Conjectured yes [Aaronson, 2020]

17 of 51

The Busy Beaver Challenge (bbchallenge)

Launched in 2022

Goal: collaboratively solving the conjecture “BB(5) = 47,176,870”
Consists of: website, Discord server, forum, wiki, galaxy of GitHub repositories

https://bbchallenge.org

18 of 51

The Busy Beaver Challenge (bbchallenge)

Launched in 2022
Goal: collaboratively solving the conjecture “BB(5) = 47,176,870”
Consists of: website, Discord server, forum, wiki,
Online, async, almost exclusively communicating on Discord
No management: “entropically-driven research”

Even the formal proof happened through a grassroot initiative

47,000 website unique visitors, ~50 daily
1000+ members on Discord
50,000+ messages exchanged
~50 active contributors
19 contributors whose contribution made it to the Coq proof
Galaxy of ~30 GitHub repositories

https://bbchallenge.org

19 of 51

The Busy Beaver Challenge

How to prove “BB(5) = 47,176,870” ?

Enumerate all 5-state Turing machines

There are 10,000 billion 5-state Turing machines

20 of 51

The Busy Beaver Challenge

How to prove “BB(5) = 47,176,870” ?

Enumerate all 5-state Turing machines

There are 10,000 billion 5-state Turing machines
“Only” 181,385,789 after symmetries and pruning

21 of 51

The Busy Beaver Challenge

How to prove “BB(5) = 47,176,870” ?

Enumerate all 5-state Turing machines

There are 10,000 billion 5-state Turing machines
“Only” 181,385,789 after symmetries and pruning�

Craft automated proof strategies

Deciders: programs that, given a TM output one of:��HALTS DOESN’T HALT UNKNOWN��→ 6 deciders used in the proof

22 of 51

The Busy Beaver Challenge

How to prove “BB(5) = 47,176,870” ?

Enumerate all 5-state Turing machines

There are 10,000 billion 5-state Turing machines
“Only” 181,385,789 after symmetries and pruning�

Craft automated proof strategies

Deciders: programs that, given a TM output one of:��HALTS DOESN’T HALT UNKNOWN��→ 6 deciders used in the proof

Try another decider

23 of 51

The Busy Beaver Challenge

How to prove “BB(5) = 47,176,870” ?

Enumerate all 5-state Turing machines

There are 10,000 billion 5-state Turing machines
“Only” 181,385,789 after symmetries and pruning�

Craft automated proof strategies

Deciders: programs that, given a TM output one of:��HALTS DOESN’T HALT UNKNOWN��→ 6 deciders used in the proof

24 of 51

The Busy Beaver Challenge

How to prove “BB(5) = 47,176,870” ?

Enumerate all 5-state Turing machines

There are 10,000 billion 5-state Turing machines
“Only” 181,385,789 after symmetries and pruning�

Craft automated proof strategies

Deciders: programs that, given a TM output one of:��HALTS DOESN’T HALT UNKNOWN��→ 6 deciders used in the proof�

Individually prove the machines that are left�� → 13 “Sporadic Machines” in the proof

25 of 51

The Busy Beaver Challenge

Deciding the undecidable: this is impossible (there is no universal decider)

26 of 51

The Busy Beaver Challenge

Deciding the undecidable: this is impossible (there is no universal decider)

How impossible?

27 of 51

The Busy Beaver Challenge

Deciding the undecidable: this is impossible (there is no universal decider)

How impossible?

-complete

There is a 25-state TM that halts iff Goldbach’s conjecture is false

There is a 744-state TM that halts iff the Riemann hypothesis is false

There is a 748-state TM that halts iff ZF is not consistent

[Code Golf Addict, 2016], [Leng, 2025]

[Matiyasevich and O’Rear, 2016]

[O’Rear, 2017]

[Riebel, 2023]

28 of 51

The Busy Beaver Challenge

Deciding the undecidable: this is impossible (there is no universal decider)

Let’s do it anyway!!

(Hope was that 5-state machines do not encode unsolvable problems)

29 of 51

The Busy Beaver Challenge

Deciding the undecidable: this is impossible (there is no universal decider)

Let’s do it anyway!!

(Hope was that 5-state machines do not encode unsolvable problems)

(Or else, we would have found the simplest open problem in maths, not bad either)

30 of 51

The Busy Beaver Challenge

Since 2022, contributors produced dozens of deciders, in many languages: �C, C++, Go, rust, Haskell, PhP, Python

bbchallenge is not proof assistant-centric
At the start, I only dreamnt we’d have some formal proofs one day (I thought 5 years)

��

31 of 51

The Busy Beaver Challenge

Since 2022, contributors produced dozens of deciders, in many languages: �C, C++, Go, rust, Haskell, PhP, Python

bbchallenge is not proof assistant-centric
At the start, I only dreamnt we’d have some formal proofs one day (I thought 5 years)

��

Instead we were using a strict validation process for deciders:

Requiring 2 independent implementations with matching results
Requiring 1 latex proof of correctness of the decider

32 of 51

Proof Assistants

But quickly, contributors with proof assistant skills joined:

In 2022, Nathan Fenner started writing deciders in Dafny�

33 of 51

Proof Assistants

But quickly, contributors with proof assistant skills joined:

In 2022, Nathan Fenner started writing deciders in Dafny�
In 2023, Maja Kądziołka started writing deciders in Coq, goal was to extract�them to OCaml for performance. The project is called busycoq and also contains the proofs of 12 out of the 13 sporadic machines�

34 of 51

Proof Assistants

But quickly, contributors with proof assistant skills joined:

In 2022, Nathan Fenner started writing deciders in Dafny�
In 2023, Maja Kądziołka started writing deciders in Coq, goal was to extract�them to OCaml for performance. The project is called busycoq and also contains the proofs of 12 out of the 13 sporadic machines�
In 2024, using Coq, mxdys:

translated, improved and created new deciders
implemented the enumeration of 5-state TMs
proved the 13th sporadic machine (~10,000 lines)

That way, mxdys proved in Coq BB(5) = 47,176,870, the proof is called Coq-BB5

35 of 51

Proof Assistants

The difficult part is to prove that the deciders are correct: for each decider we need to show that if the decider says that a machine does not halt then, the machine indeed does not halt.��Also need to prove that the enumeration is correct: that the set of 181,385,789 enumerated machines is sufficient to deduce the value of BB(5).

36 of 51

Coq-BB5

Released by mxdys in 2024, uses Coq v8.20
About 20,000 lines of Coq code (+ ~10,000 lines for imported busycoq proofs)
Implements the enumeration of TMs directly in Coq
Contains 6 deciders�

Method

https://github.com/ccz181078/Coq-BB5

37 of 51

Coq-BB5

Released by mxdys in 2024, uses Coq v8.20
About 20,000 lines of Coq code (+ ~10,000 lines for imported busycoq proofs)
Implements the enumeration of TMs directly in Coq
Contains 6 deciders�
Initially compiled in 13 hours (on a laptop)
Improved to 45 minutes by Yannick Forster

Leverage tree structure of the enumeration to paralelise the proof� → compilation time could be reduced arbitrarily using this technique
Use coq_native engine�

https://github.com/ccz181078/Coq-BB5

38 of 51

Coq-BB5

Released by mxdys in 2024, uses Coq v8.20
About 20,000 lines of Coq code (+ ~10,000 lines for imported busycoq proofs)
Implements the enumeration of TMs directly in Coq
Contains 6 deciders�
Initially compiled in 13 hours (on a laptop)
Improved to 45 minutes by Yannick Forster

Leverage tree structure of the enumeration to paralelise the proof� → compilation time could be reduced arbitrarily using this technique
Use coq_native engine�

Output: proof extracted to OCaml in order to output the list of enumerate machines together with halting status and decider ID.

https://docs.bbchallenge.org/CoqBB5_release_v1.0.0/

https://github.com/ccz181078/Coq-BB5

39 of 51

Coq-BB5

https://github.com/ccz181078/Coq-BB5

40 of 51

Coq-BB5

https://github.com/ccz181078/Coq-BB5

Lower bound: easy

Upper bound: hard

Run enumeration
Call deciders
Solve remaining�sporadic machines

41 of 51

Coq-BB5

https://github.com/ccz181078/Coq-BB5

Coq-BB5 uses one standard axiom: functional extensionality

42 of 51

Summary: landscape of small BB values

Legend��Proved in Coq�

Existence of a “Cryptid”

https://bbchallenge.org/antihydra

43 of 51

Summary: landscape of small BB values

Legend��Proved in Coq�

Existence of a “Cryptid”

Iterate Collatz-like function starting from 8:

3x/2 if even
(3x-1)/2 if odd

Do you ever get twice as many more odd terms than even ones?

Antihydra halts iff this is true.

6-state TM
Simplest open problem in mathematics, on the�BB scale

https://bbchallenge.org/antihydra

44 of 51

Future work

Next BB values (although hopeless)

~4,000 machines left to solve in BB(6), over 33B total
~80 machines left to solve in BB(2,5)
6 machines left to solve in BB(3,3), including a machine that we believe is halting�

Legend��Proved in Coq�

Existence of a “Cryptid”

45 of 51

Future work

Next BB values (although hopeless)

~4,000 machines left to solve in BB(6), over 33B total
~80 machines left to solve in BB(2,5)
6 machines left to solve in BB(3,3), including a machine that we believe is halting�
There are still open questions about 5-state machines

Legend��Proved in Coq�

Existence of a “Cryptid”

46 of 51

5-state machine zoo

47 of 51

5-state machine zoo��

Machine Skelet #1��Cycles after 10^51 steps�Period is ~10^9 steps

48 of 51

5-state machine zoo

Machine Skelet #10��Double Fibonacci counter

49 of 51

5-state machine zoo

Machine Skelet #17��Does Gray Code under�many layers of obfuscation

50 of 51

Credits, many thanks to all bbchllaenge Collaborators

New contributors welcome!

Special thanks to Maja Kądziołka for some of her slides!

https://sakamoto.pl/~mei/bbslides/bbslides.html

51 of 51

Thank you very much!!

Do you have any questions :) ?

The first draft of the BB5 paper is out, feedback welcome!

https://github.com/bbchallenge/bbchallenge-paper

Slides, links and more

I am open to work