Lispers learned marketing, bravo!
The only issue is the missing credit to the Quanta article https://www.quantamagazine.org/how-godels-incompleteness-the....
Went through the quanta article -- it seems reasonably different (doesn't go deep on how proof, subst, work, etc) -- I suspect the similarities stem from both of us reading Nagel and Newman's book.
The article "What Gödel Discovered" improves on the Quanta
article linked above by using Lisp expressions instead of
Gödel numbers.
The proof in "What Gödel Discovered" is still incorrect
because the Lisp expressions it uses leave out the crucial
orders on propositions in Russell's Principia Mathematica.