有没有 token 用不完的佬一起做几何定理证明器

9 月 18 日
 bombless
想要支持的证明大概是这样的 https://github.com/AxiomMath/IMO2026/blob/main/IMO2026/Q2/solution.lean
但是要做可视化

当前只有自然数的证明，效果在 https://bombless.github.io/prover-typescript/

我目前还在免费的 luna 上手工 loop 推进，还没提交
1253 次点击
所在节点    数学
6 条回复
metalvest
9 月 18 日
是可以 AI 接入然后调用的吗
bombless
9 月 18 日
@metalvest 是计算机辅助证明，属于是形式化证明，是严格数学推导的
c4tn
9 月 18 日
怎么参与
niubee1
9 月 18 日
我有不限量的 DeepSeek V4.1 Flash 和 GLM5.3 Flash
bombless
9 月 18 日
@c4tn 给 https://github.com/bombless/prover-typescript/发 pull request 就行。到时候把权限调一下每个 pr 显示对应的 github.io 内容的话就可以看到每个 pr 的效果了
XuHuan1025
9 月 19 日
如果是 codex 不要想用不完怎么办。同事每个月平均用六七成 sub2 看额度平均 3300 最高有 5000 。最近拉满了跑两周 额度只有 1900 了。

这是一个专为移动设备优化的页面（即为了让你能够在 Google 搜索结果里秒开这个页面），如果你希望参与 V2EX 社区的讨论，你可以继续到 V2EX 上打开本讨论主题的完整版本。

https://v2ex.ih06.com/t/1243063

V2EX 是创意工作者们的社区，是一个分享自己正在做的有趣事物、交流想法，可以遇见新朋友甚至新机会的地方。

V2EX is a community of developers, designers and creative people.

© 2021 V2EX