[[[
 Show that a formal system of complexity N
 can't prove that a specific object has
 complexity > N + 4872.
 Formal system is a never halting lisp expression
 that output pairs (lisp object, lower bound
 on its complexity).  E.g., (x 4) means
 that x has complexity H(x) greater than or equal to 4.
]]]
 
[Here is the prefix.]
 
define pi
 
let (examine pairs)
    if atom pairs false
    if < n cadr car pairs
       car pairs
       (examine cdr pairs)
 
let t 0
 
let fas nil
 
let (loop)
  let v try t 'eval read-exp fas
  let n + 4872 length fas
  let p (examine caddr v)
  if p car p
  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
[Size pi + fas.]
length
append bits pi
       bits 'display '(xyz 9999)
[Here pi finds something suitable.]
 
cadr try no-time-limit 'eval read-exp
append bits pi
       bits 'display '(xyz 5073)
[Here pi doesn't find anything suitable.]
 
cadr try no-time-limit 'eval read-exp
append bits pi
       bits 'display '(xyz 5072)