With Fifth Busy Beaver, Researchers Approach Computation’s Limits
(www.quantamagazine.org)

from tedu@inks.tedunangst.com to inks@inks.tedunangst.com on 02 Jul 17:46

https://inks.tedunangst.com/l/5131

from tedu@inks.tedunangst.com to inks@inks.tedunangst.com on 02 Jul 17:46

https://inks.tedunangst.com/l/5131

Today, the team declared victory. They’ve finally verified the true value of a number called BB(5), which quantifies just how busy that fifth beaver is. They obtained the result — 47,176,870 — using a piece of software called the Coq proof assistant, which certifies that mathematical proofs are free of errors.

threaded - newest