問題タブ [lean]

私は、自動化された証明に依存するプロジェクトを行うことに興味があります。これは学習演習として非常に重要です。これまでのところ、私のオンライン検索では、理論的にはリーンが進むべき道であることが示唆されています。

しかし、私がそれについて読んだのは、VS コードまたは Emacs で証明アシスタントとして使用することについて話しているだけです。しかし、それは私が必要としているものではありません。プログラムで完全に通信できるシステムが必要です。仮定のIE文字列が入ります->控除可能性を指定する文字列が出てくるか、そのようなものです。

より正確に言うと、一連の結果が入力された仮定から推定できるかどうかを判断するという重い作業を行う文字列の解析関数を呼び出せるようにする必要があります。

リーンがこれを行うことができるというドキュメントが見つかりません。