Roger Penrose famously from Gödel's Incompleteness Theorem, that human mind is not computable, because mathematical intuition is not computable (a mathematician can prove more than any formal system, and therefore any computer).
But when I read through the proof or derivation of Gödel's First Incompleteness Theorem (say, in Penrose's The Emperor's New Mind or at plato.stanford.edu), it just happens to have been written by a human. In priciniple, a Large Language Model could write the same book or article (maybe not now, but almost surely in 10 years).
Why is a mathematician's mind not computable and the LLM is computable given that 1) they both produce proofs as sequences of natural language mixed with mathematical formalism, 2) any proof produced by a human can be produced, in principle, by an LLM (being the same sequence of natural language mixed with formal mathematics)?