>>368
形式的証明を検証するプログラムの名前。
プログラムに理解できるよう形式的証明に書き直して検証させれば、あとは機械的に正しい証明になっているかいないか判定してくれる。
自分でプログラムを通して正しいと確認できたなら、その形式的証明を上げれば、同じプログラムで誰もが正しいと確認できる。