アカウント名:
パスワード:
人間であれ、証明支援系であれ、実際の証明の確認に伴う演算は、必ず物理系を通して行われる。
実行時の物理系の内部状態に対する無知から、物理系を用いた計算は必ず0でない有限の確率で間違う。
従って、ある証明が科学的に正しいと主張する時は、証明が正しい確率を示さなければならない。
何年もかかるような計算の時はなおさらである。
ソフトウェア工学のようにプログラムのテストや数学の証明にバグが残っている可能性とか、コンパイラや定理証明系にバグがある可能性とか計算機が誤動作や故障する確率というのを探求してもいいかもしれないね。論文に誤りがあるかもしれないからレビューや検証がなされるわけだし。追試によって論文の信ぴょう性が確かめられるというか
チェッカーの完全解析 [sciencemag.org]の時には、計算結果を保存するHDDの故障率がかなり重要なファクターになっていて朝、研究室に来るとどの部分のディスクが飛んでいて、どの部分の計算をやり直さなくてはならないかチェックするのが日課になっていたと言う話を聞いたことがあります。ウェブで見たのですが、リンク先を見つけられなかった。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
犯人は巨人ファンでA型で眼鏡をかけている -- あるハッカー
数学者が言う証明完了は科学的に誤りである (スコア:0)
人間であれ、証明支援系であれ、実際の証明の確認に伴う演算は、必ず物理系を通して行われる。
実行時の物理系の内部状態に対する無知から、物理系を用いた計算は必ず0でない有限の確率で間違う。
従って、ある証明が科学的に正しいと主張する時は、証明が正しい確率を示さなければならない。
何年もかかるような計算の時はなおさらである。
Re: (スコア:0)
ソフトウェア工学のようにプログラムのテストや数学の証明にバグが残っている可能性とか、
コンパイラや定理証明系にバグがある可能性とか
計算機が誤動作や故障する確率というのを探求してもいいかもしれないね。
論文に誤りがあるかもしれないからレビューや検証がなされるわけだし。
追試によって論文の信ぴょう性が確かめられるというか
Re:数学者が言う証明完了は科学的に誤りである (スコア:1)
チェッカーの完全解析 [sciencemag.org]の時には、計算結果を保存するHDDの故障率がかなり重要なファクターになっていて
朝、研究室に来るとどの部分のディスクが飛んでいて、どの部分の計算をやり直さなくてはならないか
チェックするのが日課になっていたと言う話を聞いたことがあります。
ウェブで見たのですが、リンク先を見つけられなかった。