[[[ 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)