doc: update Freek Wiedijk's list

[iehality]

Add information about formalized proof of Gödel's incompleteness theorem to Freek Wiedijk's list, which was missing before.

---

[jcommelin]

Congratulations with this formalization!
As far as I can see, you have formalized the first incompleteness theorem.
Looking at the entries of other formalizations in Freek's list, they seem to include both the first and second incompleteness theorem. Do you have plans to also formalize the 2nd?

[iehality]

Proving a full second incompleteness theorem like the one proved in isabelle seems much more difficult and not tackle on yet.
The second incompleteness theorem, assuming the derivability conditions (like the proof in coq) is being worked on in one of the PR. It seems that proof in HOL only shows the first incompleteness theorem.

[Vierkantor]

We have discussed this among the maintainers: the consensus is that we also want the second incompleteness theorems before we consider the goal to be achieved. I am very happy to see these theorems being formalized in Lean, so I hope that this encourages you to make a completer formalization.

[iehality]

Thank you. I am currently working on the full-proof of the second incompleteness theorem and will request it again when completed.