alright just for fun: AMA but only about math, will attempt to speed-explain stuff with as few symbols and equations as possible and see what happens
(esp happy to field questions about stuff that seems basic to you and that you feel like you should've gotten a long time ago!)
Conversation
so, you can write down a function l(P) that given a proposition P in some formal system outputs the length of the shortest proof of P (and maybe throws an error if P isn't provable or something). and you can consider L(n), the maximum of l(P) over all statements P of length n
1
6
for reasonably powerful formal systems, eg peano arithmetic, L(n) grows faster than any computable function!
because if it was bounded by a computable function then you could use that function to determine which statements are provable (by checking all proofs up to that length)
2
4
Replying to
yeah the argument is very similar although i have to think for a bit about whether the exact version i just stated is true. this version is definitely true and very famous:
en.wikipedia.org/wiki/Entscheid