Inter-universal geometryとABC予想(シン応援スレ) 92 (434ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
411(2): 07/22(水)10:56 ID:u5VrSqGL(2/8) AAS
>>258
そもそも証明検証ツールが本格的に運用されるようになったのは今世紀以降。
いかなる非形式的証明もギャップが無いことが検証されていない。
それでも数学者は長年培ってきた数学的思考によりたいていの証明につきギャップの有無を判断できる。
ところがIUTは既存の数学とは全く異なる言語で記述されており長年の経験が役に立たない。
そのようなIUT固有の事情を考慮せずに
>時代が進まないと、ギャップに気付かないということは
>数学史上しばしばあった
などと言ったところでまったく的外れ。
>代数学の基本定理（＝代数方程式は複素数根を持つ）
省2
414(1): 07/22(水)13:53 ID:n+1eBk57(1/2) AAS
>>411
>そもそも証明検証ツールが本格的に運用されるようになったのは今世紀以降。
ショルツがやったやったやつみたいに
ホッカホカの最新の数学が検証されたのはたしかに最近
>いかなる非形式的証明もギャップが無いことが検証されていない。
これは言い過ぎでIsabelle, HOL, Coqは前世紀から使われてるし
利用する公理の範囲を検討する逆数学との関係で
ギャプ探しは結構行われてた
415(2): 07/22(水)13:54 ID:n+1eBk57(2/2) AAS
>>411
>ところがIUTは既存の数学とは全く異なる言語で記述されており長年の経験が役に立たない
これも大した問題じゃない
ギャプがあると問題だけど
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.023s