#lean 4 のAIニュース

DeepSeek、再帰的証明探索と新ベンチマークでニューラル定理証明を進展させる「DeepSeek-Prover-V2」を発表

DeepSeek AIは、Lean 4環境での形式定理証明専用大規模言語モデル「DeepSeek-Prover-V2」を公開した。同モデルは再帰的定理証明パイプラインを採用し、DeepSeek-V3から高品質な初期データを生成することで最先端の性能を実現した。