你的前瞻/资源到底是大于1还是小于1:
2024年底我们在ai产品之外做了自动化融合lean4定理证明服务，想要为一般数学，计算机和物理学者的科研服务，用尽奇技淫巧融合了几十篇paper的思想把miniF2F score从四五十刷到了60多实际上算不小的成功。
但没有任何转化成用户体验和生产价值。
2025年 ds的prover model把这个分数用强化学习提到了90+ 随后各家的frontier model自动化定理证明可以被很好的耦合在一个非常简洁的定理证明循环里达到很高的质量
2026年 openai 在此之上用一万个朴素的这样的loop近似解了ns（还没被坐实）。
陶老师这种顶级人类已经开始讲math2.0。
所以，前瞻性乘上错配的资源，就是没有后勤没有保障的情况下攻上甘岭。那个山头被范弗利特式火力覆盖，你没有赢的可能。
想像志愿军一样赢，你要打好地道。
@aigc1024
2024年底我们在ai产品之外做了自动化融合lean4定理证明服务，想要为一般数学，计算机和物理学者的科研服务，用尽奇技淫巧融合了几十篇paper的思想把miniF2F score从四五十刷到了60多实际上算不小的成功。
但没有任何转化成用户体验和生产价值。
2025年 ds的prover model把这个分数用强化学习提到了90+ 随后各家的frontier model自动化定理证明可以被很好的耦合在一个非常简洁的定理证明循环里达到很高的质量
2026年 openai 在此之上用一万个朴素的这样的loop近似解了ns（还没被坐实）。
陶老师这种顶级人类已经开始讲math2.0。
所以，前瞻性乘上错配的资源，就是没有后勤没有保障的情况下攻上甘岭。那个山头被范弗利特式火力覆盖，你没有赢的可能。
想像志愿军一样赢，你要打好地道。
@aigc1024
