10年以上を費やしていた「ケプラー予想」の証明が完了し、その内容が正しいことが示されたそうだ(GIZMODO)。
ケプラー予想は、ケプラーの法則で知られる数学者/天体物理学者ヨハネス・ケプラーが提唱した、空間上に球体を充填する際に最高密度となる充填方法。1998年にトマス・ヘールズ氏によってその証明が示されていたのだが、その内容は非常に複雑で、その正しさを示すことができなかったという。そのため、へールズ氏は2003年に自身で証明支援ツールを使った「答え合わせ」を開始。それがやっと終了し、証明が正しいことが実証されたという。
果物屋のオヤジ (スコア:4, すばらしい洞察)
よい方法はなかったという事でいいんですかね。
Re:果物屋のオヤジ (スコア:1)
オヤジは最密に積むことを目的にしていたのだろうか。
果物が傷みにくい積み方なのかもしれない。
果物が崩れにくい積み方なのかもしれない。
もし傷みにくいとか崩れにくいとかが理由だったとして、最密であることと関係あるのだろうか。
夏休みの自由研究になるかな?
まずはオヤジへのインタビューと果物調達だな。
スイカ買ってくる。
Re: (スコア:0)
むしろ「なるべくスカスカで見た目はギッシリ」な充填法を追求してるのではないだろうか。
何年前だったか… (スコア:2)
ピーター・フランクル氏が某マンガ雑誌にコラム記事を連載していたのですが
そのとき採り上げられた問題(話題)の一つがこのユークリッド空間での球充満法でしたね。
あの当時は、充満させるパターンはいくつかあるがどれが最適なのかは分っていない
と言うことだったはずですが、解決したんですね。
如何なる内容であろうとACでの書き込みは一切無視します。
Re:何年前だったか… (スコア:1)
よーし、次は非ユークリッド空間だ。
強い重力場の中とかイメージすればいいのかな。
Re: (スコア:0)
3次元以上の高次元だと成り立たないようですが、
24次元とかになると数式みても、
イメージする手がかりすらないな(笑)
Re:何年前だったか… (スコア:2)
>3次元以上の高次元だと成り立たないようですが、
球の充填だったら、もとより3次元のようなきがするのですが。
Re:何年前だったか… (スコア:2)
数学の話ですので、もっと一般化された球のことです。
2次元だと我々の知る「円」、3次元で普通の「球」、
4次元以上では「超球」と呼ばれます。
Re:何年前だったか… (スコア:1)
>3次元以上の高次元
4次元以上の間違いだと言いたかったんだと思います。申し訳ない。
以下、以上、未満、超過、の使い分けが日本語の口語ではアバウトですよね・・・
FAQ (スコア:1)
証明が正しいことの証明が正しいことはどうやって証明したんですか?
Re:FAQ (スコア:4, 参考になる)
複雑な証明の場合、その正しさは「確認」されます。
この場合のことは詳しくは知らないのですが、証明が非常に多くの場合分けや多くの補題の組合せに
なっていて、それらの組合せや場合分けが必要十分であることが「答え合わせ」で確認された
と考えればよいと思います。
で、その確認というは計算機実験で証明に挙げられている場合以外が出てこないということを
時間をかけてしらみつぶしで確認するなどが行われます。
Re: (スコア:0)
証明の土台としていきつくのが公理系で、公理は証明するものじゃない
Re: (スコア:0)
証明が正しいことの証明が正しいことは、
すでに正しいことが証明されているので、
証明する必要がありません。
4色問題 (スコア:1)
"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, 参考になる)
似てますよね。今後もより良い充填方法は見つからないことは示されたけど、それが何故なのかは未だに未解決、みたいな。
4色問題も、何故4になるのかは分からないままで、最小値が存在してそれがたまたま4だったのか、4である事に意味があるのかが不明。
似たような結果になるかと危惧されていたフェルマーの大定理が、3という数字に深い意味が見いだされて決着が付いたのとは対照的。
Re:4色問題 (スコア:1)
せっかく証明したのに誰も自分の名前で定理を呼んでくれないワイルズさんカワイソス
Re: (スコア:0)
ペレルマンさんはむしろペレルマンの定理とか呼ばれたら嫌がりそうだ
Re: (スコア:0)
未だに未解決、みたいな。
数学者が言う証明完了は科学的に誤りである (スコア:0)
人間であれ、証明支援系であれ、実際の証明の確認に伴う演算は、必ず物理系を通して行われる。
実行時の物理系の内部状態に対する無知から、物理系を用いた計算は必ず0でない有限の確率で間違う。
従って、ある証明が科学的に正しいと主張する時は、証明が正しい確率を示さなければならない。
何年もかかるような計算の時はなおさらである。
Re: (スコア:0)
その確率を計算する方法は、過去に正しいと証明された方法だと思いますが、その計算方法が正しい確率はいくらくらいでしょうか。
Re: (スコア:0)
数学自体は科学じゃないので大丈夫です。
Re: (スコア:0)
コンピュータのメモリがビット反転起こして計算が間違ってるかもしれないって意味ですか?
Re: (スコア:0)
これについての反論を書きかけたんだけど、途中でアホらしくなってきた
夏だなあ、という感想ばかり浮かんできちゃうんだけど、真面目に突っ込んだほうがいいのこれ?
Re:数学者が言う証明完了は科学的に誤りである (スコア:1)
大学には哲学とかいうこの種の屁理屈ばかりこねまわしている学問があると聞いて
Re:数学者が言う証明完了は科学的に誤りである (スコア:1)
哲学はすべての学問の根源で哲学者がいちばん偉いんだ
みたいな事を言ってた教授が居たけど、哲学やってる
人たちって言葉の定義をはっきりさせずに議論している
バカな人たちって印象。数学はこの数百年、思考を
はっきりさせるために記号化などを推し進めてきたけど、
哲学はそれすらしないでぐだぐだ言ってるだけ。
Re: (スコア:0)
そうではなく、古来、医学と神学を除く他の学問は全部「哲学」だった。(今でも自然科学の学位取ると「XXX of Philosophy」って言うよね)
そこから、文学、自然科学、その他、役に立つ研究分野が次々とスピンアウトしていった結果、最後に「無用なもの」だけが残った。これが現代哲学。
記号化などを進めて…などという研究分野は、「哲学」からどんどんスピンアウトしてしまっているのです。
よって、現代哲学は学問としてこの上なく純粋であり、かつ役立たずなのです。
Re: (スコア:0)
自分は屁理屈だと思ったが、それは正しいのだろうか? なんて考えていくと、哲学ですね。
Re: (スコア:0)
ソフトウェア工学のようにプログラムのテストや数学の証明にバグが残っている可能性とか、
コンパイラや定理証明系にバグがある可能性とか
計算機が誤動作や故障する確率というのを探求してもいいかもしれないね。
論文に誤りがあるかもしれないからレビューや検証がなされるわけだし。
追試によって論文の信ぴょう性が確かめられるというか
Re:数学者が言う証明完了は科学的に誤りである (スコア:1)
チェッカーの完全解析 [sciencemag.org]の時には、計算結果を保存するHDDの故障率がかなり重要なファクターになっていて
朝、研究室に来るとどの部分のディスクが飛んでいて、どの部分の計算をやり直さなくてはならないか
チェックするのが日課になっていたと言う話を聞いたことがあります。
ウェブで見たのですが、リンク先を見つけられなかった。
Re: (スコア:0)
残念、あなたの主張は、大昔にデカルトが本に書いて発表してます。
「三角形の内角の和が180度だなんて、悪魔がそう思い込ませてるだけかもしれないじゃないか」と、当時としてはいちゃもんとしか言い様のないことを主張してます。
Re: (スコア:0)
レジのお姉さんに言ってあげてください。
Re: (スコア:0)
>ある証明が科学的に正しいと主張する時は、
誰もそんな主張はしてないと思いますよ。
数学的に正しいと主張しているだけで。
証明支援イザベルさん (スコア:0)
どんなキャラなんだろう。
閃きはないけど、ひたすら定理を検証してくれる優秀な助手って感じだろうか。
Re: (スコア:0)
否。人間の間違いを指摘しつづける小言幸兵衛。
だれか女性キャラを探して。
Re: (スコア:0)
「アホらし」とか「バカばっか」とか言う少女に一票
副産物はないのかな (スコア:0)
やっぱり、「あらゆるパターンを調べ上げる」過程で、意外な良い積み方が見いだされたりはしなかったんでしょうか。
普通に頑張って積み上げようとしている分にはまず試さないような奇妙な積み上げ方が、
最適ではないけど結構良い線まで行く事を発見して、「その発想は無かった」的な驚きがいくつか得られるとか、
充填率では劣るけど、別の尺度では優れた積み上げ方を見いだすとか。
そういう発見が無く、当たり前の積み上げ方が当たり前に最強だという結果を淡々と調べ続けるのは、相当に地味な作業になりそうで。
まあ、証明系を改良したりぶん回したりと、エキサイティングな作業ではあるんでしょうけど。
Re:副産物はないのかな (スコア:5, 参考になる)
> 意外な良い積み方が見いだされたりはしなかったんでしょうか
一つの玉に最大何個の玉がくっつけられるか、というのが接吻数で、(三次元の)玉の場合12個です。
ケプラー予想の配置パターンでは、玉の赤道上に6つを輪にしてならべ、その上下に3つづつ三角に置く配置です(上下の三角が同じ向きか上下逆さまかで2パターンが有る)。
その他の12個配置として、北極南極に一つづつおき北半球と南半球に5つの輪にして置くパターンがあり、この配置の場合中心以外の玉同士の間にあるていどの隙間をいれて配置することができます。
ケプラー配置では全ての玉が密着していてぐらつかないけど、後者の配置は隙間があるため無限のパターンが考えられることになります。
そしてこれらの隙間を集めて玉をもう一つ入れられる隙間ができるのか(できない)、がヘールズの証明のキモでもあったりします。
ヘールズの証明は、配置パターンを調べあげるというより、この隙間のように配置で取りうる制約(不等式)を並べあげることで、計算機に与えて解かせる線形計画法となっています。
あと記事にリンクがあってしかるべきだと思うけど、以下が該当プロジェクトでのアナウンスで、そこには各ソースコードも公開されてます。
https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion [google.com]
Re: (スコア:0)
> あと記事にリンクがあってしかるべきだと思うけど、
まったくタレコミACの手抜きぶりにも困ったものですね。あ、もちろんへールズまで完コピしたhylomさんの仕事は完璧で非のうちどころもありませんよ。
なんか関連ストーリーに変なのが湧いてるな (スコア:0)
http://science.srad.jp/comments.pl?sid=579440&cid=2235067 [srad.jp]
> NP問題であるという事を示すのに天才数学者は別にいりません。
> 定義から、どのような問題でも多項式時間で自動証明検証ができる場合は(NP完全かはともかく)NP問題に当てはまります。
> 証明が有限長を持ち、各ステップの妥当性がアルゴリズムで検証できる場合はそうです。
お前が多項式時間計算可能と計算可能の区別もついていないことはよくわかった。
> 少なくとも一般人が「数学」や「証明」といった場合、有効な書かれた証明を持ち、その正しさは客観的かつ一意に判定できる分野を指すでしょう。
> そこに一階述語論理と書いてあるのはまさに、ゲーデルの不完全性定理から健全性かつ完全性を持つ二階述語論理にそのような条件が当てはまらないからです。
お前がリンク先の文章を全く理解できないで自分に都合のいい脳内解釈にこじつけているだけなのが改めてよくわかった。
> 数学の世界がどうなっているか余り詳しいわけではないので、普通に数学的証明と云える範囲で、多項式時間で機械的検証ができないような例があればご教授いただきたいところです。
チューリング機械の停止問題。そこまで持ち出さなくても計算量クラスEXPTIME以上の問題全て。
計算量クラスの定義からほとんど自明なことを人に聞いている時点でお前が何もわかっていないしわかってもいないことについて知ったかぶりすることがよくわかった。
トンデモさんに何言っても無駄なのはわかっているがあえてもう一度言うと、お前は定理の自動証明について二度と語るな。
Re:へ(ひらがな)ールズ (スコア:1)
OCRとか、パッドで手書き入力とか
Re:へ(ひらがな)ールズ (スコア:1)
日本語変換だと良くありますよ。
「~へ」とか「~は」という助詞の後に、カタカナ語として成り立つものを置くとなりやすい。
例えば、「ヘンリー」だとまず起きないけど、「ヘリンダ」だと「へリンダ」になりがち。
Re: (スコア:0)
この場合前が「、」で後が「ー」なんですけど。
Re:へ(ひらがな)ールズ (スコア:1)
最初の2文字が感動詞の「へー」と認識されて、後ろの2文字は未知の語としてカタカナに変換、という流れはありそう。
この頃のIMEって、見慣れない仮名並びに遭遇するとカタカナを上位に挙げてきますよね。