戻る

> However, over the last few years myself and hundreds of other mathematicians in the Lean community have spent many many thousands of person-hours building a digitised library mathlib ([mC20]) of standard undergraduate, Masters and early PhD level mathematics, so this is going to change.

ここ数年で私含め Lean コミュニティの何百人もの数学者がものすごい労力をかけて学部・修士・博士レベルの数学の形式化 (定理証明支援系のライブラリ実装) を行ってきたので、こういった (問題のある) 状況も変わっていくだろう。