xv01

https://mathlib-initiative.org/ from https://www.renaissancephilanthropy.org/funds 用于「科研」, 商业化 ( 「刚需」 ) 其实是很少的 ... right ?

======

Ironically interesting to see LLM vibe proving !! https://axiommath.ai/territory/from-seeing-why-to-checking-everything

For humans, we have decent intuitions. We know problems with heavy case analysis are tedious to enumerate. We know problems requiring one clever construction can make one stuck forever or shout aha! But for machines, we're still in the dark. A real theory of machine difficulty—what structural features make problems easy or hard for automated provers – seems like a genuinely interesting research direction.

Right now the workflow is simple: humans pose problems, machines find proofs. But you can imagine something more interactive. Machines sanity-checking human ideas in real time. Humans reviewing machine feedback and steering search toward promising directions. Each side complementing the other.

Axiom is building a world where human intuitions are grounded by machine verification and machine verification in turn inspires human intuitions.

这也是一种「涌现」么

还记得 傅立叶变换 实现 同余加法 么 ?

https://x.com/xleaps/status/1627873094814531584

& https://twitter.com/xleaps/status/1627844991824297984

====== ​ ​组合数学的特点在于杂。组合题类型丰富 , 没有「标准工具」且很大程度上依赖非常巧妙的观察 , 因此在数学竞赛和信息学竞赛中也常常被认为是衡量一个人「思维能力」的标准之一

而没有 标准工具 证明灵活 即使不考虑 AI , 仅对编写 Lean 代码的人 , 也会是不小的挑战

​... AlphaProof ​把大量的时间浪费在了细枝末节上 , 而非组合问题中那一两步关键的充满灵感的数学构造 https://www.zhihu.com/question/662586636/answer/3577050463 ​ ​组合题相对灵活 , 不需要太多复杂的定理和公式 , 需要的是将问题抽象化和转换的能力 , 这也是为什么 IMO 和 IOI 双栖选手往往在组合题中得分较高的原因