Deep respect for Natalie Wolchover's mind and writing, and the best popsci version of Gödel's famous proof I have seen, but I'm skeptical that a non-initiate can fully understand the article, and also about how she ties the proof to her own epistemology. quantamagazine.org/how-godels-inc…
I liked the Gödel numbers when I had to work through the proof as an undergrad, but it requires acquiring a bit of number theory and a little arithmetic trickery to see how and why Gödel got to this elegant but inefficient solution to tokenizing mathematical source code.
For a cursory understanding, it's probably better to encode expressions as byte strings like everyone else and bring home how an automatic process can operate on the bytes to produce syntactic changes that correspond to the semantics.
But how do the symbols (syntax) get their meaning (semantics)? This part is probably the core insight of computer science and makes computation congruent with constructive mathematics. It's missing in the article, and crucial to understanding what Gödel actually shot down.
Most of us have good intuitions about the relationship between symbols and interpretation in computational machines, so it makes sense to skip climbing this hill. But that makes the core insight that there can be no mathematical semantics beyond what's computable harder to see.
Largest obstacle in the text appeared to me to be the slightly buggy explanation of the Gödelization, and the sudden appearance and treatment of the somewhat inscrutable substitution operator, which does not even show up in the earlier defined Gödel number alphabet.
If the reader skips over this part and does not pause to fully understand both the sub operator's implementation (which is hard without realizing that Gödel just carried us in a computational paradigm) and its prime number encoding, the rest of the explanation will be a jumble.
Because the last few paragraphs become comprehensible again, I fear that the article might leave readers in an incomprehending but positively bewildered state of semi enlightenment: we have met a mystery that remained a mystery but nevertheless tasted a deep sense of insight.
This is also the note on which the article ends: The meaning of incompleteness is deeply important but sadly unfathomable to mortal minds. Is Gödel's proof (accessible to CS undergrads before math education) the deepest achievement and last frontier of mathematical ingenuity?
It is as if Chaitin, Solomonoff and Schmidhuber had never lived. Chaitin explains incompleteness as a problem of data compression: proving means compressing a statement to its axioms. This requires an algorithm that gives a result in a finite time.
It turns out that classical math semantics define truth in a non computable manner. Gödel and Turing show that if you build a machine using any math to this specification, it will crash. If we want to build a language to speak about truth, we need a different definition of truth.
Does Natalie Wolchover's text correctly imply what to think about the implications for our understanding of physics? Gödel does not restrict the reach of mathematics in describing the world, he discovers the restrictions of models in which anything can think about the world.
PS: Chaitin's 1987 paper "The complete arithmetization of EVAL" that derives a diophantine equation with 17000 variables to compute the state transitions of a Lisp interpreter has to be one of most scurrilous interactions between math and computer science ever.
