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

Home Sign Up Sign In

This topic created in 50 days ago, the information mentioned may be changed or developed.

想要支持的证明大概是这样的 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

Sep 18

1

是可以 AI 接入然后调用的吗

bombless

OP

Sep 18

2

@metalvest 是计算机辅助证明，属于是形式化证明，是严格数学推导的

c4tn

Sep 18 via iPhone

3

怎么参与

niubee1

Sep 18

4

我有不限量的 DeepSeek V4.1 Flash 和 GLM5.3 Flash

bombless

OP

Sep 18

5

@c4tn 给 https://github.com/bombless/prover-typescript/发 pull request 就行。到时候把权限调一下每个 pr 显示对应的 github.io 内容的话就可以看到每个 pr 的效果了

XuHuan1025

Sep 19

6

如果是 codex 不要想用不完怎么办。同事每个月平均用六七成 sub2 看额度平均 3300 最高有 5000 。最近拉满了跑两周额度只有 1900 了。

About · Help · Advertise · Blog · API · FAQ · Privacy · Solana · 1507 Online Highest 6679 ·

Select Language

创意工作者们的社区

World is powered by solitude

VERSION: 3.9.8.5 · 28ms · UTC 11:50 · PVG 19:50 · LAX 03:50 · JFK 06:50
♥ Do have faith in what you're doing.