Drawing Blanks

Premature Optimization is a Prerequisite for Success

Busy beavers defeat Infinity

with one comment

This simple fact is a striking revelation for me:



Basically, any decidable property of the natural numbers (a PI_1 formula) can be proved by a computer, by brute force. The program wouldn’t need to check all the numbers. If it runs longer than the busy beaver while looking for a counterexample, it will never find one.

This includes, by the way, proving consistency of formal systems: Con(F) is a PI_1 formula; we can write a program that checks each natural number for being the proof number for “1=0”.

UPDATE (6 years later):

The 8000th Busy Beaver number eludes ZF set theory: new paper by Adam Yedidia and me

they built an actual Turing machine that won’t halt only if ZF is consistent.
As a side benefit, machines that can prove Goldbach’s Conjecture and the Riemann Hypothesis by searching a _finite_ segment of N for counterexamples.


Chaitin’s “Computing the Busy Beaver Function” is now available at this URL:


or google for pdf containing the following:

In T. M. Cover and B. Gopinath, Open Problems in Communication and Computation, Springer, 1987






Written by bbzippo

09/09/2010 at 2:01 am

Posted in math, programming

One Response

Subscribe to comments with RSS.

  1. […] Systems that have enough knowledge about certain aquatic rodents are Π1-complete (no kidding). […]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: