Gödelの第一不完全性定理の形式的証明をする(外部記事)
https://zenn.dev/palalansouki/articles/d3ec6573bbc2c8
iehality/lean4-logic