Godel's incompleteness theorem

Stream: general

[Mark Gerads]

I was wondering if Godel's incompleteness theorem has been formalized in any computer logic system, and thought here would be a good place to bring up the topic. I am interested in this because, while I understand the gist of the argument, am afraid a subtle loophole might disallow the self-referential Godel number from existing. I would thus like to see this formalized, though formalizing it myself is currently beyond me.

[Eric Rodriguez]

some proofs are here: https://www.cs.ru.nl/~freek/100/ (thm 6)

[Eric Rodriguez]

it's not been done in Lean yet afaik

[Mark Gerads]

Thank you.

[Eric Wieser]

I've just noticed that the word "constructive" on Freek's site leads to a chaotic neutral domain squatter who sent me to an ad the first time I clicked it, to a bing search for "intuitionism" the second time, and a search for "isa investments" the third time.

[Eric Wieser]

@Freek Wiedijk, I assume whatever you were linking to is no longer there!

[Eric Rodriguez]

it was his website it seems from the web archive :(

[David Michael Roberts]

@Mark Gerads see https://www.isa-afp.org/entries/Incompleteness.html