« 8/14の秘密のケンミンショーで千葉 木更津の謎のフライと大阪のイカ焼きを紹介。 | トップページ | フリーマン・ダイソンさんのものすごく貴重なインタビューが! »

2014年8月14日 (木)

お!ケプラー予想、とうとう証明が検証されたのか。ただしコンピュータによる証明検証。

400年の難問、「ケプラー予想の証明」やっと100%終わる

という記事が。証明が出たのはだいぶ前だったけれど、ようやく検証されたのか。

で使われているのがコンピュータによる証明支援システム。

HOL lightと、、、

http://www.cl.cam.ac.uk/~jrh13/hol-light/

Isabelle

http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html

Ocaml(Objactive CAML)を使っているって。

http://ja.wikipedia.org/wiki/OCaml

これからこういう証明が増えていくのかな。

コンピュータでエルデシュのある問題を証明させたら、人間が検証できないほど巨大(13GB)になったというお話が!

というのもあるし。

« 8/14の秘密のケンミンショーで千葉 木更津の謎のフライと大阪のイカ焼きを紹介。 | トップページ | フリーマン・ダイソンさんのものすごく貴重なインタビューが! »

日記・コラム・つぶやき」カテゴリの記事

コメント

コメントを書く

(ウェブ上には掲載しません)

トラックバック

この記事のトラックバックURL:
http://app.cocolog-nifty.com/t/trackback/512682/60151339

この記事へのトラックバック一覧です: お!ケプラー予想、とうとう証明が検証されたのか。ただしコンピュータによる証明検証。:

« 8/14の秘密のケンミンショーで千葉 木更津の謎のフライと大阪のイカ焼きを紹介。 | トップページ | フリーマン・ダイソンさんのものすごく貴重なインタビューが! »

無料ブログはココログ
2017年4月
            1
2 3 4 5 6 7 8
9 10 11 12 13 14 15
16 17 18 19 20 21 22
23 24 25 26 27 28 29
30            

最近のコメント

フォト