フォワード・リーズニングとバックワード・リーズニング - 檜山正幸のキマイラ飼育記 (はてなBlog)現状の証明支援系〈proof assistant〉について、僕はしょっちゅう愚痴と文句を言っています（twitterでぼやいたりしてる）。大きな不満点は、フォワード・リーズニングの対話的サポートがまったくない点です。不便だし面白くない。 内容： 証明ソフトウェアの進歩は遅い バックワード・リーズニング フォワード・リーズニング フォワード・リーズニングの対話的サポート 証明ソフトウェアの進歩は遅い 「プログラミング言語Lean 4の現状」に書いたように、証明ソフトウェアの開発は膨大な時間と手間がかかるもので、Coq, Isabelle, Mizar は30年から50年ほどの開発期間を経ています。新しいソフトウェアであるLeanでも、もう10年になります。どの開発チームも最優秀の人材を揃えています。それでも「使いものにならない」事実が、証明ソフトウェアの開発が極めて困難であることを物語ってい
