>> His precise theorem is this: Define "LISP program-size complexity" to be the size of a LISP subroutine that examines a proof, determines whether it is correct, and returns either the theorem established by the proof (if the proof is correct) or an error message (if the proof is incorrect). Then, given a formal axiomatic system A, with LISP program-size complexity N, A cannot be used to prove that any LISP expression longer than N + 356 characters is elegant.
Doesn't this in fact prove that numbers are discovered, not invented?
Doesn't this in fact prove that numbers are discovered, not invented?
He defines elegance to be "N". He defines
N = 1
356 + N != N
Thus, real numbers are real.