Kimi 发布 Kimina-Prover Preview 形式化推理模型

Kimi 发布 Kimina-Prover Preview，称其为首个能以类人方式推理并在 Lean 4 语言中严格证明数学定理的大型形式化推理模型。官方同时列出了该模型设计与训练的关键要点，并附论文链接 http://arxiv.org/abs/2504.11354。