前回の記事で私はこんなことを書きました．
Lean で数値計算ができるようになればもっと多くの層が取り込めることが期待できるのですが，現状では難しそうです．
改めて考えてみると，数値計算は丸め誤差と打ち切り誤差がどうしてもついてまわるため形式証明とは相性が悪いはずで，Lean で数値計算ができるようになってもあまり嬉しくないかもしれません．ちょっと勘違いをしていました．すみません．
私個人としては静的型付け言語で数値計算をしたいなと思っている *1 ので，数値計算も Lean でやりたいモチベがあるんですが，Julia でやるより特段便利になることはないかもしれないということです．
それはそれとして，Python の Sage のような記号計算は形式証明とも相性がいいはずで，それは Lean でやる価値があるはずです．実際 mathlib にある polyrith というタクティクは Sage を呼び出して利用します．（ちゃんと証明もします）そうやって，他の記号計算ライブラリを呼び出して Lean 内部で利用する方法が確立されれば，一気に Lean でできることが増えるかもしれません．
*1: Julia も静的型付けではなさそう
