そういやペーター・ショルツェが割と最近コンピュータによる定理自動証明について書いていた。
現代数学の最先端で使えるレベルになっているものも出てきたらしいよ