26/07/22 13:53:33.89 n+1eBk57.net
>>411
>そもそも証明検証ツールが本格的に運用されるようになったのは今世紀以降。
ショルツがやったやったやつみたいに
ホッカホカの最新の数学が検証されたのはたしかに最近
>いかなる非形式的証明もギャップが無いことが検証されていない。
これは言い過ぎでIsabelle, HOL, Coqは前世紀から使われてるし
利用する公理の範囲を検討する逆数学との関係で
ギャプ探しは結構行われてた
26/07/22 13:53:33.89 n+1eBk57.net
>>411
>そもそも証明検証ツールが本格的に運用されるようになったのは今世紀以降。
ショルツがやったやったやつみたいに
ホッカホカの最新の数学が検証されたのはたしかに最近
>いかなる非形式的証明もギャップが無いことが検証されていない。
これは言い過ぎでIsabelle, HOL, Coqは前世紀から使われてるし
利用する公理の範囲を検討する逆数学との関係で
ギャプ探しは結構行われてた