前回の記事で私はこんなことを書きました．
改めて考えてみると，数値計算は丸め誤差と打ち切り誤差がどうしてもついてまわるため形式証明とは相性が悪いはずで，Lean で数値計算ができるようになってもあまり嬉しくないかもしれません．
しかしSciLean というライブラリの使い方を書いた文書
を読んでいると，Leanで数値計算をするメリットが書かれていて驚きました．Lean のような依存型がある言語で数値計算ができると，型で仕様を表現できるので他の言語にはない利便性が提供できるという話だったと思います．
考えてみると，数値計算が得意な言語と言えば Julia 言語かなと思うのですが，実際に Julia を触ってみると動的型付けであることや #eval コマンドに相当するものがないことが不満に思えるので，Lean で数値計算ができれば嬉しいですね．形式証明と数値計算の相性は悪くても，依存型システムとは必ずしも相性が悪くないかもしれません．
この SciLean というライブラリの今後の開発動向は要チェックだと思います．
