« 科学者の残した言葉などをコミックにした"ドミトリーともきんす"(高野文子さん)、今日が最終回でした。 | トップページ | USA Todayの方が日本のメディアより浅田真央ちゃんの頑張りをよく伝えているという、、、 »

2014年2月21日 (金)

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

Computer generated math proof is too large for humans to check

という記事が出てました。

Erdős discrepancy problem

というのがあって、±1の値をとる数列x1,x2,..と任意の値Cについて、

 \left| \sum_{i=1}^k x_{id} \right| > C

が成り立つk,dがあるか?

というもの。これをコンピュータで証明させたという論文。

A SAT Attack on the Erdos Discrepancy Conjecture

証明に使ったプログラムはこれらのようです。

http://fmv.jku.at/lingeling/

http://www.labri.fr/perso/lsimon/glucose/

SATソルバーってのがあるんですね。

http://bach.istc.kobe-u.ac.jp/aisat.html

数独を解いたりしている例が、、、

http://d.hatena.ne.jp/ku-ma-me/20080108/p1

脱線した。

で得られた結果が13GBだって、、、人間が検証できないという、、、

« 科学者の残した言葉などをコミックにした"ドミトリーともきんす"(高野文子さん)、今日が最終回でした。 | トップページ | USA Todayの方が日本のメディアより浅田真央ちゃんの頑張りをよく伝えているという、、、 »

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

コメント

コメントを書く

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

トラックバック

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

この記事へのトラックバック一覧です: コンピュータでエルデシュのある問題を証明させたら、人間が検証できないほど巨大(13GB)になったというお話が!:

« 科学者の残した言葉などをコミックにした"ドミトリーともきんす"(高野文子さん)、今日が最終回でした。 | トップページ | USA Todayの方が日本のメディアより浅田真央ちゃんの頑張りをよく伝えているという、、、 »

最近の記事

最近のコメント

2017年12月
          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
31            
フォト
無料ブログはココログ