3月マルレク「コンピュータ、数学の問題を解き始める」について
【 3月マルレク「コンピュータ、数学の問題を解き始める」について 】 3月のマルレクは、「コンピュータ、数学の問題を解き始める」というテーマで開催しようと思っています。 この2月に、Deepmind / Open-AIはとても興味深い発表を行いました。 「数学オリンピックの形式的問題(のいくつか)を解く」 "Solving (Some) Formal Math Olympiad Problems" https://openai.com/blog/formal-math/ 国際数学オリンピックのいくつかの問題をコンピュータを使って解いて見せたのです。 たとえば、こんな感じです。 問題(2000年の数学オリンピックの問題だそうです) Prove that if |x - 2| = p, where x < 2, then x - p = 2 − 2p. ( |x - 2| = p とする。 x < 2 の時、x - p = 2 - 2p となることを証明せよ。) 証明 Since x < 2, |x - 2| = - (x - 2). Using p = |x - 2| , we have x = 2 − p and finally x - p = 2− 2p. ( x < 2 なので、|x - 2| = - (x - 2)である。p = |x - 2| を使えば、x = 2 − p である。結局、x - p = 2− 2p となる。) 先の論文には、この例をふくめて6つの例が紹介されています。実際には、コンピュータは、形式的証明を返すのですが、ここで紹介したのは、「非形式的 Informal」な証明です。マシンは、Informal ボタンを押すと、こうした「非形式的」証明を返してくれます。形式的証明を非形式的証明へ要約・翻訳できるのも面白いです。 Deepmindは、数学へのAIの利用について、昨年12月、Natureにこんな論文を発表していました。それは、数学者に向けてAIも使いみちがあると述べたものでしたが、今回の発表は、そうした関心と方法の延長線上にあるものだと思います。ただ、今回の方が訴求力は大きいように思います。 "Advancing mathematics by guiding human