[[[
Show that a formal system of complexity N
can't determine more than N + 8000 + 7328
= N + 15328 bits of Omega.
Formal system is a never halting lisp expression
that outputs lists of the form (1 0 X 0 X X X X 1 0).
This stands for the fractional part of Omega,
and means that these 0,1 bits of Omega are known.
X stands for an unknown bit.
]]]
[Here is the prefix.]
define pi
let (number-of-bits-determined w)
if atom w 0
+ (number-of-bits-determined cdr w)
if = X car w
0
1
let (supply-missing-bits w)
if atom w nil
cons if = X car w
read-bit
car w
(supply-missing-bits cdr w)
let (examine w)
if atom w false
[if < n (number-of-bits-determined car w)]
[ Change n to 1 here so will succeed. ]
if < 1 (number-of-bits-determined car w)
car w
(examine cdr w)
let t 0
let fas nil
let (loop)
let v try t 'eval read-exp fas
let n + 8000 + 7328 length fas
let w (examine caddr v)
if w (supply-missing-bits w)
if = car v success failure
if = cadr v out-of-data
let fas append fas cons read-bit nil
(loop)
if = cadr v out-of-time
let t + t 1
(loop)
unexpected-condition
(loop)
[Size pi.]
length bits pi
[Run pi.]
cadr try no-time-limit 'eval read-exp
append bits pi
append [Toy formal system with only one theorem.]
bits 'display '(1 X 0)
[Missing bit of omega that is needed.]
'(1)