BB(5) Proven in Coq

[Shawn Ligocki]

bbchallenge.org just announced a Coq proof of the 5-state (2-symbol) Busy Beaver problem. The step champion remains the Marxen and Buntrock 1990 TM which runs for 47,176,870 steps and leaves 4098 1s on the tape.

Ben Brubaker at Quanta has written up a lovely history of the BB(5) problem.

We are currently working on writing up our results for formal publication.

[Shawn Ligocki]

Also,

• Blog post by Scott Aaronson about the new result: https://scottaaronson.blog/?p=8088
• HackerNews post: https://news.ycombinator.com/item?id=40857041