一、教程简介

DeepSeek-Prover-V2-7B 是由深度求索团队于 2025 年 5 月 1 日发布的专为数学 AI 编程语言 Lean 4 打造的开源大语言模型。它的最大特点是能够将非形式化的数学推理（即人类常用的推理方式）和严格的形式化证明无缝结合，让模型既能像人类一样灵活思考，又能像计算机一样严谨论证，实现了数学推理的一体化融合。相关论文成果为 DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition 。

本教程采用资源为单卡 A6000，该模型仅支持数学推理问题。

二、项目示例

三、运行步骤

1. 启动容器后点击 API 地址即可进入 Web 界面

若不显示「模型」，这表示模型正在初始化，由于模型较大，请等待约 1-2 分钟后刷新页面。

2. 进入网页后，即可与模型展开对话

使用步骤

四、交流探讨

🖌️ 如果大家看到优质项目，欢迎后台留言推荐！另外，我们还建立了教程交流群，欢迎小伙伴们扫码备注【SD 教程】入群探讨各类技术问题、分享应用效果↓

项目支持

感谢 Github 用户 xxxjjjyyy1  对本教程的部署。