明日はcoq-community/goedel及びRussel O'Connor; "Essential Incompleteness of Arithmetic Verified by Coq"を読みLean4に移植可能かどうかを見てみたい

https://github.com/coq-community/goedel