Kimina-Prover-Preview: 首个能以类人方式进行推理并在 Lean 4 语言中严格证明数学定理的大型形式化推理模型。

技术报告： github.com/MoonshotAI/Kimina-Prover-Preview/

这是Numina 与合作的首个面向 Lean 4 的大型形式化推理模型。 ​​​