結局、「人間が書いた１千行の証明」を「２０万行の完全証明」に
自動変換するシステムが必要になるな。