パスワードを忘れた? アカウント作成
11461672 story
数学

ケプラー予想の証明が完了 44

ストーリー by hylom
16年経過 部門より
あるAnonymous Coward 曰く、

10年以上を費やしていた「ケプラー予想」の証明が完了し、その内容が正しいことが示されたそうだ(GIZMODO)。

ケプラー予想は、ケプラーの法則で知られる数学者/天体物理学者ヨハネス・ケプラーが提唱した、空間上に球体を充填する際に最高密度となる充填方法。1998年にトマス・ヘールズ氏によってその証明が示されていたのだが、その内容は非常に複雑で、その正しさを示すことができなかったという。そのため、へールズ氏は2003年に自身で証明支援ツールを使った「答え合わせ」を開始。それがやっと終了し、証明が正しいことが実証されたという。

この議論は賞味期限が切れたので、アーカイブ化されています。 新たにコメントを付けることはできません。
  • 果物屋のオヤジ (スコア:4, すばらしい洞察)

    by NOBAX (21937) on 2014年08月15日 13時27分 (#2657085)
    彼が店頭でリンゴやミカンを積み上げて売っているのより、
    よい方法はなかったという事でいいんですかね。
    • by Anonymous Coward on 2014年08月15日 15時19分 (#2657160)

      オヤジは最密に積むことを目的にしていたのだろうか。
      果物が傷みにくい積み方なのかもしれない。
      果物が崩れにくい積み方なのかもしれない。
      もし傷みにくいとか崩れにくいとかが理由だったとして、最密であることと関係あるのだろうか。

      夏休みの自由研究になるかな?
      まずはオヤジへのインタビューと果物調達だな。
      スイカ買ってくる。

      親コメント
      • by Anonymous Coward

        むしろ「なるべくスカスカで見た目はギッシリ」な充填法を追求してるのではないだろうか。

  • by LoadFF (27414) on 2014年08月15日 14時13分 (#2657113)

    ピーター・フランクル氏が某マンガ雑誌にコラム記事を連載していたのですが
    そのとき採り上げられた問題(話題)の一つがこのユークリッド空間での球充満法でしたね。
    あの当時は、充満させるパターンはいくつかあるがどれが最適なのかは分っていない
    と言うことだったはずですが、解決したんですね。

    --
    如何なる内容であろうとACでの書き込みは一切無視します。
  • by Anonymous Coward on 2014年08月15日 13時06分 (#2657073)

    証明が正しいことの証明が正しいことはどうやって証明したんですか?

    • Re:FAQ (スコア:4, 参考になる)

      by new release (37404) on 2014年08月15日 21時30分 (#2657425) 日記

      複雑な証明の場合、その正しさは「確認」されます。
      この場合のことは詳しくは知らないのですが、証明が非常に多くの場合分けや多くの補題の組合せに
      なっていて、それらの組合せや場合分けが必要十分であることが「答え合わせ」で確認された
      と考えればよいと思います。
      で、その確認というは計算機実験で証明に挙げられている場合以外が出てこないということを
      時間をかけてしらみつぶしで確認するなどが行われます。

      親コメント
    • by Anonymous Coward

      証明の土台としていきつくのが公理系で、公理は証明するものじゃない

    • by Anonymous Coward

      証明が正しいことの証明が正しいことは、
      すでに正しいことが証明されているので、
      証明する必要がありません。

  • by Anonymous Coward on 2014年08月15日 13時26分 (#2657083)

    "Hales の証明は、コンピュータを使ってあらゆる個々のケースを調べつくすという方法" https://ja.wikipedia.org/wiki/%E7%90%83%E5%85%85%E5%A1%AB#.E7.90.83.E5... [wikipedia.org]
    発想・手法としては4色問題と同じなのね。 https://ja.wikipedia.org/wiki/4%E8%89%B2%E5%95%8F%E9%A1%8C [wikipedia.org]
    Coqというのも使えるのかな? https://ja.wikipedia.org/wiki/Coq [wikipedia.org]
    もしかして「証明支援ツール」というのがそれ?

    • Re:4色問題 (スコア:2, 参考になる)

      by Anonymous Coward on 2014年08月15日 14時31分 (#2657128)

      似てますよね。今後もより良い充填方法は見つからないことは示されたけど、それが何故なのかは未だに未解決、みたいな。
      4色問題も、何故4になるのかは分からないままで、最小値が存在してそれがたまたま4だったのか、4である事に意味があるのかが不明。

      似たような結果になるかと危惧されていたフェルマーの大定理が、3という数字に深い意味が見いだされて決着が付いたのとは対照的。

      親コメント
      • by Anonymous Coward on 2014年08月15日 14時35分 (#2657131)

        せっかく証明したのに誰も自分の名前で定理を呼んでくれないワイルズさんカワイソス

        親コメント
        • by Anonymous Coward

          ペレルマンさんはむしろペレルマンの定理とか呼ばれたら嫌がりそうだ

      • by Anonymous Coward

        未だに未解決、みたいな。

  • by Anonymous Coward on 2014年08月15日 13時21分 (#2657079)

    人間であれ、証明支援系であれ、実際の証明の確認に伴う演算は、必ず物理系を通して行われる。

    実行時の物理系の内部状態に対する無知から、物理系を用いた計算は必ず0でない有限の確率で間違う。

    従って、ある証明が科学的に正しいと主張する時は、証明が正しい確率を示さなければならない。

    何年もかかるような計算の時はなおさらである。

    • by Anonymous Coward

      その確率を計算する方法は、過去に正しいと証明された方法だと思いますが、その計算方法が正しい確率はいくらくらいでしょうか。

    • by Anonymous Coward

      数学自体は科学じゃないので大丈夫です。

    • by Anonymous Coward

      コンピュータのメモリがビット反転起こして計算が間違ってるかもしれないって意味ですか?

    • by Anonymous Coward

      これについての反論を書きかけたんだけど、途中でアホらしくなってきた
      夏だなあ、という感想ばかり浮かんできちゃうんだけど、真面目に突っ込んだほうがいいのこれ?

      • by Anonymous Coward on 2014年08月15日 14時46分 (#2657141)

        大学には哲学とかいうこの種の屁理屈ばかりこねまわしている学問があると聞いて

        親コメント
        • by Anonymous Coward on 2014年08月15日 20時45分 (#2657405)

          哲学はすべての学問の根源で哲学者がいちばん偉いんだ
          みたいな事を言ってた教授が居たけど、哲学やってる
          人たちって言葉の定義をはっきりさせずに議論している
          バカな人たちって印象。数学はこの数百年、思考を
          はっきりさせるために記号化などを推し進めてきたけど、
          哲学はそれすらしないでぐだぐだ言ってるだけ。

          親コメント
          • by Anonymous Coward

            そうではなく、古来、医学と神学を除く他の学問は全部「哲学」だった。(今でも自然科学の学位取ると「XXX of Philosophy」って言うよね)
            そこから、文学、自然科学、その他、役に立つ研究分野が次々とスピンアウトしていった結果、最後に「無用なもの」だけが残った。これが現代哲学。
            記号化などを進めて…などという研究分野は、「哲学」からどんどんスピンアウトしてしまっているのです。

            よって、現代哲学は学問としてこの上なく純粋であり、かつ役立たずなのです。

        • by Anonymous Coward

          自分は屁理屈だと思ったが、それは正しいのだろうか? なんて考えていくと、哲学ですね。

    • by Anonymous Coward

      ソフトウェア工学のようにプログラムのテストや数学の証明にバグが残っている可能性とか、
      コンパイラや定理証明系にバグがある可能性とか
      計算機が誤動作や故障する確率というのを探求してもいいかもしれないね。
      論文に誤りがあるかもしれないからレビューや検証がなされるわけだし。
      追試によって論文の信ぴょう性が確かめられるというか

    • by Anonymous Coward

      残念、あなたの主張は、大昔にデカルトが本に書いて発表してます。
      「三角形の内角の和が180度だなんて、悪魔がそう思い込ませてるだけかもしれないじゃないか」と、当時としてはいちゃもんとしか言い様のないことを主張してます。

    • by Anonymous Coward

      レジのお姉さんに言ってあげてください。

    • by Anonymous Coward

      >ある証明が科学的に正しいと主張する時は、

      誰もそんな主張はしてないと思いますよ。

      数学的に正しいと主張しているだけで。

  • by Anonymous Coward on 2014年08月15日 13時44分 (#2657099)

    どんなキャラなんだろう。
    閃きはないけど、ひたすら定理を検証してくれる優秀な助手って感じだろうか。

    • by Anonymous Coward

      否。人間の間違いを指摘しつづける小言幸兵衛。
      だれか女性キャラを探して。

    • by Anonymous Coward

      「アホらし」とか「バカばっか」とか言う少女に一票

  • by Anonymous Coward on 2014年08月15日 14時41分 (#2657137)

    やっぱり、「あらゆるパターンを調べ上げる」過程で、意外な良い積み方が見いだされたりはしなかったんでしょうか。

    普通に頑張って積み上げようとしている分にはまず試さないような奇妙な積み上げ方が、
    最適ではないけど結構良い線まで行く事を発見して、「その発想は無かった」的な驚きがいくつか得られるとか、
    充填率では劣るけど、別の尺度では優れた積み上げ方を見いだすとか。

    そういう発見が無く、当たり前の積み上げ方が当たり前に最強だという結果を淡々と調べ続けるのは、相当に地味な作業になりそうで。

    まあ、証明系を改良したりぶん回したりと、エキサイティングな作業ではあるんでしょうけど。

    • by Anonymous Coward on 2014年08月15日 17時42分 (#2657285)

      > 意外な良い積み方が見いだされたりはしなかったんでしょうか

      一つの玉に最大何個の玉がくっつけられるか、というのが接吻数で、(三次元の)玉の場合12個です。
      ケプラー予想の配置パターンでは、玉の赤道上に6つを輪にしてならべ、その上下に3つづつ三角に置く配置です(上下の三角が同じ向きか上下逆さまかで2パターンが有る)。

      その他の12個配置として、北極南極に一つづつおき北半球と南半球に5つの輪にして置くパターンがあり、この配置の場合中心以外の玉同士の間にあるていどの隙間をいれて配置することができます。
      ケプラー配置では全ての玉が密着していてぐらつかないけど、後者の配置は隙間があるため無限のパターンが考えられることになります。

      そしてこれらの隙間を集めて玉をもう一つ入れられる隙間ができるのか(できない)、がヘールズの証明のキモでもあったりします。
      ヘールズの証明は、配置パターンを調べあげるというより、この隙間のように配置で取りうる制約(不等式)を並べあげることで、計算機に与えて解かせる線形計画法となっています。

      あと記事にリンクがあってしかるべきだと思うけど、以下が該当プロジェクトでのアナウンスで、そこには各ソースコードも公開されてます。

      https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion [google.com]

      親コメント
      • by Anonymous Coward

        > あと記事にリンクがあってしかるべきだと思うけど、

        まったくタレコミACの手抜きぶりにも困ったものですね。あ、もちろんへールズまで完コピしたhylomさんの仕事は完璧で非のうちどころもありませんよ。

  • by Anonymous Coward on 2014年08月17日 18時12分 (#2658218)

    http://science.srad.jp/comments.pl?sid=579440&cid=2235067 [srad.jp]
    > NP問題であるという事を示すのに天才数学者は別にいりません。
    > 定義から、どのような問題でも多項式時間で自動証明検証ができる場合は(NP完全かはともかく)NP問題に当てはまります。
    > 証明が有限長を持ち、各ステップの妥当性がアルゴリズムで検証できる場合はそうです。

    お前が多項式時間計算可能と計算可能の区別もついていないことはよくわかった。

    > 少なくとも一般人が「数学」や「証明」といった場合、有効な書かれた証明を持ち、その正しさは客観的かつ一意に判定できる分野を指すでしょう。
    > そこに一階述語論理と書いてあるのはまさに、ゲーデルの不完全性定理から健全性かつ完全性を持つ二階述語論理にそのような条件が当てはまらないからです。

    お前がリンク先の文章を全く理解できないで自分に都合のいい脳内解釈にこじつけているだけなのが改めてよくわかった。

    > 数学の世界がどうなっているか余り詳しいわけではないので、普通に数学的証明と云える範囲で、多項式時間で機械的検証ができないような例があればご教授いただきたいところです。

    チューリング機械の停止問題。そこまで持ち出さなくても計算量クラスEXPTIME以上の問題全て。
    計算量クラスの定義からほとんど自明なことを人に聞いている時点でお前が何もわかっていないしわかってもいないことについて知ったかぶりすることがよくわかった。
    トンデモさんに何言っても無駄なのはわかっているがあえてもう一度言うと、お前は定理の自動証明について二度と語るな。

typodupeerror

計算機科学者とは、壊れていないものを修理する人々のことである

読み込み中...