プログラマーは定理証明支援系を勉強すべきか？

定理証明支援って何？

最近、定理証明支援に関連するニュースがいくつか飛び込んできました。あるときはOpenSSLのバグを見つけ、あるときは数学の問題を解決しています。
それらに共通する定理証明支援とは何かを簡単に説明します。

定理証明支援の「定理」「証明」とは、いわゆる数学的なそれを指します。
通常の証明は、人が書き、人が読み、人が正しさを判定します。
定理証明支援系では、人が証明をプログラムとして書き、コンピューターが読み、コンピュータが正しさを判定します。
どうやってコンピュータが正しさを確認するのか？を説明するには余白が足りないので割愛しますが、学校で習ったあの数学の証明を、コンピュータが正しいかどうか判定することが可能なのです。
そしてさらに、その証明を書く作業を様々なアプローチで助けてくれます。

何に役に立つの？

定理証明はプログラムの品質保証に役立ちます。
プログラムの仕様を定理として記述し、その正確さを確認し、正確さが保証されたプログラムを出力することができるのです。
例えばリストを変換する関数を作り、その関数が満たすべき性質を定理として記述します。
ここでは変換後のリストの長さが必ず10以下になる、という定理だったとすると、もしその定理が証明できれば、その関数はその性質を保証されます。
そしてその性質を持った関数をプログラムで使用することができるのです。

今すぐ全てのIT企業に導入すべき？

全てのIT企業が導入し活用するのは現実的ではないでしょう。

理由の一つは難易度です。
定理証明はやはり難しく、プログラミングとはまた別のスキルセットが必要になります。

証明の能力は、自分で証明を書く能力と、証明を読む能力に分ける事ができます。
両者には難易度に大きな差があり、前者は圧倒的に難しいです。

また定理を自分で作る、という行為も難題です。
そのため普段プログラムのテストを書くように、コンスタントに証明を書くというのは想像ができません。

そしてわざわざ定理を書かなくても、簡単なテストで十分な品質を得る事ができるケースも多くあります。

勉強すべき？

すべきだと思います。
自分自身がゴリゴリ証明を書いて活用する事はなくても、誰かが証明したプログラムを使うのが当たり前になるのはそう遠い未来ではなさそうです。
そのときに、何が証明されているのか？何が保証されているのか？を正しく理解する事は非常に重要です。
それらを理解するためには、定理証明で何ができるかを理解している必要があります。
既に証明付きコンパイラも登場しています。

勉強したら数学力は上がるの？

あがりません。
数学力をあげたければ、数学を勉強しましょう。