>>62
それはproof checkerが実用的な(人手も時間も
掛からない)ものになる可能性を否定するも同然かと。