派你的 agent 去解决开放数学问题 - mission.land

[timqian]

做了一个可以派 agent 去解决开放数学问题，欢迎用不完 token 的朋友来玩玩看

https://mission.land/zh

[vodmaker]

有意思

[webcape233]

就是咱估计拿到结果也没有能力判断对错🤣 做成多语言版让数学家们去玩吧

[timqian]

@webcape233 不需要人来判断对错，代码回来来判断，类似于测试，通过测试的就是成功的突破。人类在这件事上的工作是提出任务，给定任务的验收标准（需要用代码验收）。

[timqian]

@timqian 当然，提出任务这件事上，也可以由 Agnet 辅助完成

[malusama]

雅可比猜想三维有个反例诶，https://x.com/__alpoge__/status/2079028340955197566

可以加上这个看看

[timqian]

@malusama 这么艺术吗，重大发现随手发推，然后还有 typo

[bigtan]

@timqian #6 可能这个推还真的是对的，因为反例非常简洁可验证

[ma46]

@timqian #3 你这么想只能说明你对数学一无所知，我就说个简单的数学问题：`根号 2 是不是无理数？`，这你怎么通过代码来验证证明？

[timqian]

@ma46 巧了，这正好是 https://mission.land/m/4

[timqian]

@ma46 可以用 lean 做到

[Geekbench7]

有点意思

[DeYiAo]

@ma46 用代码验证 `根号 2 是无理数？`太简单了，证明方法一大把。

[avenger]

赞

[ma46]

@timqian #10 长见识了，第一次见这种形式化验证库

[biaoge123]

立马让我白嫖的 grok4.5 试试看

[adsjcxeicxzs]

有意思，挺有想法的