scrapbox 上で Peano playground というのを始めて、比較的かんたんな定理を完全に形式的に証明してみようと思っていろいろ作業してみたところ、自分は形式的に証明できる定理が何一つ無いということに気付いた。