AgdaによるGalois理論のプログラミング

摘要

数学の証明に計算機を使うのは既に古い歴史がある。Agda[5]は定理証明支援系だが、普通の関数型プログラミング言語でもあり、群の要素の数え上げなどを直接に実行できる。この時に「正しく数え上げのか」ということが問題になる。4色問題が計算機を使って解かれた時にも検算[4]が問題になった。