deepseek-prover-v2在温度为0，top_p为1时的结果为1、2、10、13、15对，其余错误，使用模型为OpenRouter
第一题正确：
第二题正确：
第三题错误：
第四题错误：
第五题错误：
第六题错误：
第七题错误：
第八题错误：
第九题错误：
第十题正确：
第十一题错误：
第十二题错误：
第十三题正确：
第十四题错误：
第十五题正确：
第二题正确：
第三题错误：
第四题错误：
第五题错误：
第六题错误：
第七题错误：
第八题错误：
第九题错误：
第十题正确：
第十一题错误：
第十二题错误：
第十三题正确：
第十四题错误：
第十五题正确：
3 个赞
所有答案均为一起生成，并非单题测试
1 个赞
这玩意就不是这么用的，prover 是结合 lean 的形式语言证明工具，这一点之上甚至可能还有额外的格式要求
2 个赞
论坛里有佬友说只能用lean，也有说能用自然语言的，我就拿自然语言测一下
主要是不懂lean
用起来感觉怎么样
有点懵逼，感觉我这种小白日常肯定用不上
能用自然语言是因为 base 的底子还在，就像你问Qwen-Math 太阳从哪边升起他也能答一样，但是这种 Prover 都是高度形式语言特化的，其他问题就，看 base 的能力丢的多不多了
感谢答疑，那就当看个热闹 
1 个赞
我想用claude翻译题目来着，但是它和我说有些题目用lean需要添加额外库？我不太懂了，不懂这种语言
“以上代码中很多部分（标注 sorry 的地方）都只是示意性的，因为在 Lean 4 中完整实现这些计算和概念需要更多的库支持和详细的逻辑编写。实际应用中可能需要进一步的完善和调整。”
期待酒馆可以上
5 个赞
我了个豆樱佬，这都能酒馆啊hhh
能对着 lean4 酒馆也是神人了 
1 个赞
这。。什么水平
r1都行
什么是lean4
目测从自然语言出发解题不如v3和r1
不过楼里也有大佬说是语言不对，可能从lean出发很牛逼吧
一种计算机定理证明器
不明白。