- 497 名前：現代数学の系譜11 ガロア理論を読む [2013/03/16(土) 20:44:03.18 ]
- >>495
訂正
けど、現代人にとってはコンピュータ使うのはチート（じゃない）
↓
けど、現代人にとってはコンピュータ使うのはチートじゃない
つづき
四色問題はコンピュータによる解決だった
ja.wikipedia.org/wiki/%E5%9B%9B%E8%89%B2%E5%AE%9A%E7%90%86
1976年に ケネス・アッペル (Kenneth Appel) とヴォルフガング・ハーケン (Wolfgang Haken) は、「放電」と呼ばれる手続きを考案し、1405個の不可避集合に対してコンピュータを利用した演算を行った結果、四色定理を証明するに至った[1][2][3]。
当初は、あまりに複雑なプログラムのため他人による検証が困難であることや、ハードウェアおよびプログラムのバグの可能性を考慮して、この証明を疑問視する声があった。
その後、1996年にニール・ロバートソン (Neil Robertson) らによりアルゴリズムやプログラムの改良が行われ、より簡易な手法（従来の放電手続きよりシンプルな放電手続きを考案し、不可避集合の数を1405個から633個に抑えた）による再証明が行われた[4]。
更に、2004年にはジョルジュ・ゴンティエ (Georges Gonthier) が定理証明支援系言語である Coq を用いて、よりシンプルな証明を行った[5]。その結果、現在では四色問題の解決を否定する専門家はいなくなっている。
四色定理は実用的には地図作製だけでなく、携帯電話の基地局配置にも応用されている。周波数の同じ電波同士で混信してしまうFDMA・TDMA方式の携帯電話システムでは、隣接する基地局同士に同じ周波数を割り当てないように、配慮している。
|
 |
