News: Leaninfer リリース

[Seasawher]

https://github.com/lean-dojo/LeanInfer

タクティクを自動で提案してくれるツールのようです

[haruhisa-enomoto]

内部的にはこれはLeanDojoが公開している事前学習済みモデルを使って推論している感じなんでしょうか？

[haruhisa-enomoto]

https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/LeanInfer.3A.20Neural.20Network.20Inference.20in.20Lean.204/near/390051184
Zulipのスレ見る限りそんな感じはします
インストールめんどくさそうですがグラボ無しでも動くという記述もあり。