@dougmerritt okay, I read Chaitin's 36 page thing on the implications of a diophantine equation whose solutions depend on Chaitin's number,
tl;dr
the gist of which is that even in pure mathematics we're probably stuck going to empiricism, and that while mathematicians weren't obviously listening to him about it, with the advent of modern computing people were doing it anyway because it's something computers lend themselves to.
; he constructed lisps as practical support to his theorems