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

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

bombless 2026-09-18 20:10 1
想要支持的证明大概是这样的 https://github.com/AxiomMath/IMO2026/blob/main/IMO2026/Q2/solution.lean
但是要做可视化

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

我目前还在免费的 luna 上手工 loop 推进，还没提交
最新回复 (6)
  • metalvest 09-18 21:15
    1楼
    是可以 AI 接入然后调用的吗
  • bombless 楼主 09-18 22:19
    2楼
    @metalvest 是计算机辅助证明，属于是形式化证明，是严格数学推导的
  • c4tn 09-18 22:59
    3楼
    怎么参与
  • niubee1 09-18 23:13
    4楼
    我有不限量的 DeepSeek V4.1 Flash 和 GLM5.3 Flash
  • bombless 楼主 09-18 23:29
    5楼
    @c4tn 给 https://github.com/bombless/prover-typescript/发 pull request 就行。到时候把权限调一下每个 pr 显示对应的 github.io 内容的话就可以看到每个 pr 的效果了
  • XuHuan1025 09-19 17:16
    6楼
    如果是 codex 不要想用不完怎么办。同事每个月平均用六七成 sub2 看额度平均 3300 最高有 5000 。最近拉满了跑两周 额度只有 1900 了。
* 帖子来源V2EX
附近帖子
返回
飞读
随机推荐