bombless
V2EX  ›  数学

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

  •  
  •   bombless · 1 day ago · 863 views
    想要支持的证明大概是这样的 https://github.com/AxiomMath/IMO2026/blob/main/IMO2026/Q2/solution.lean
    但是要做可视化

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

    我目前还在免费的 luna 上手工 loop 推进,还没提交
    6 replies    2026-09-19 17:16:05 +08:00
    metalvest
        1
    metalvest  
       1 day ago
    是可以 AI 接入然后调用的吗
    bombless
        2
    bombless  
    OP
       23h 6m ago
    @metalvest 是计算机辅助证明,属于是形式化证明,是严格数学推导的
    c4tn
        3
    c4tn  
       22h 26m ago via iPhone
    怎么参与
    niubee1
        4
    niubee1  
       22h 13m ago
    我有不限量的 DeepSeek V4.1 Flash 和 GLM5.3 Flash
    bombless
        5
    bombless  
    OP
       21h 56m ago
    @c4tnhttps://github.com/bombless/prover-typescript/发 pull request 就行。到时候把权限调一下每个 pr 显示对应的 github.io 内容的话就可以看到每个 pr 的效果了
    XuHuan1025
        6
    XuHuan1025  
       4h 10m ago
    如果是 codex 不要想用不完怎么办。同事每个月平均用六七成 sub2 看额度平均 3300 最高有 5000 。最近拉满了跑两周 额度只有 1900 了。
    About   ·   Help   ·   Advertise   ·   Blog   ·   API   ·   FAQ   ·   Privacy   ·   Solana   ·   2944 Online   Highest 6679   ·     Select Language
    创意工作者们的社区
    World is powered by solitude
    VERSION: 3.9.8.5 · 34ms · UTC 13:26 · PVG 21:26 · LAX 06:26 · JFK 09:26
    ♥ Do have faith in what you're doing.