从自然语言的角度来看，数学远没有我想象中的那么严谨。




先是季度的例行公事，新番组


    

  • 日常：感谢对战～大小姐才不玩格斗游戏～(我对格斗游戏不敏感，对后面的潜水感到莫名其妙，但我就喜欢这玩意)
    • 

  • 乐队：BanG Dream! YUME∞MITA(虽然和前两作好像没啥关系，但经典延续，好像就是这个系列让我觉得3D动画也还行)
    • 

  • 少女：成长秀～向日葵马戏团～(我觉得无需多言)
    • 

  • 料理：炒翻天(感觉好久没看料理番了，狂妄的主角，我喜欢)
    • 

  • 宫廷：虽然我不是完美恶女～雏宫蝶鼠替换传～(不好评，但看在你画风好看的面上)
    • 

  • 异世界：暴走千金立誓复仇。～用魔导书之力碾碎祖国～(每季度必选)
    • 



续作组


    

  • 无职转生Ⅲ到了异世界就拿出真本事(虽然没前几季波澜，但过好日常也不赖，不能理解的是明明都口诉完了倒数第二集还得演这出吗？)
    • 

  • Re：从零开始的异世界生活 第四季 夺还篇(不知道为啥，感觉世界观越来越看不懂了，但也看得下去)
    • 

  • 超超超超超喜欢你的100个女朋友 第三季(我现在突然觉得女主并非越多越好，不然感觉水分太多，看后面作者能否把握吧)
    • 

  • 乙女游戏世界对路人角色很不友好第二季(虽然制作也不咋滴，但这是少有的我看完小说的动漫，就看看吧)
    • 



接下来进入正题吧，我遗憾地宣布我的魔群月光形式化计划破产了。资金顶不住了，这是总消耗




还有一地的垃圾


归档文件


它虽然没啥意义了，但也是烧钱烧出来的，就放出来吧。然后我来讲讲一下整个历程吧。
想法起源于这个月的几个数学大事，我觉得无需多言。于是我也想借着ai干些啥，正好openartemis的项目让我找到了用ai的手感，于是想形式化我之前研究过的一些东西，费马大定理已经被老A给干了，ns被干了，感觉庞加莱猜想(后补：就在我写完这篇文章的第二天，形式化成果就被公布了，还好我当初没选。还有就是那套工作流非常值得参考，我后面看看能不能用到国产模型上。)迟早会被盯上，我就选择了感觉无人问津的魔群月光。那时的我浑然不知，这是个大坑。
最开始我啥也不懂，还是老的那一套，资料给足随时查阅，要求一个完成魔群月光形式化，然后就是无error无超出mathlib要求公理假设等这些常规的要求。然后就是什么，ai开始猛猛地干了，一个个lean代码飞速产出的时候，我还有那么点兴奋，看着一份份进展的简报，一个个编译过的lean代码。突然觉得原来形式化是这么简单的事情吗？看来是个手到擒来的东西。但是随着lean代码越来越多的时候，我发现了不对劲，如果是程序代码堆积屎山，能运行也不会怎么样，但数学不一样，你不断堆积屎山，但啥也没用完成啊！！！是的，我们都知道ai有上下文窗口的概念，而大多数的窗口压缩算法都不咋滴，所以要提前做好规划，管理好上下文窗口与任务分配，对于这么一个大的数学定理，确实也可以做好很多规划，但是能否组织起来却没有那么简单。数学不是编程，编程写好了一个个模块，组织的不好也能编译，只是带着bug。但lean不一样，你写好了一个个模块，但最后发现永远无法完成证明，lean就不允许你编译通过，模块就组织不起来了，于是ai不断寻找补救方法，更多的lean文件堆积了起来，看似ai简报了完成了一次次难题攻克，但方向全错了，更可怕的是碰上上下文压缩，就全废了，无限的绕圈，生产一堆看似符合要求的lean却都是垃圾。那时我突然明白了，我根本就不懂lean4，其实lean的正确用法是善用sorry来标记猜想，然后一点点地去延伸证明。这其实是一点很重要的思想，nosorry成为ai的思想钢印以后，导致ai完全不敢写sorry，只能设想一条路径，脑补好需要的模块，写出一个个基础的nosorry模块以后，再进行最后的组装。但其实这完全不对，因为它设想了这个模块可能是有用的，但实际在lean4检查以后，其实根本没有用，垃圾自然就不断产生了。
这次失败以后，我换了法子，干脆先让ai把魔群月光的基础结构先搞出来，然后再从魔群月光猜想出发，一点点地往下完成证明。所以后面的目标变成了构建月光模，也就是那本FLM的核心书籍Vertex Operator Algebras and the Monster，很快ai也摸到了重点，要构造月光模，先搞定第八章的一个核心定理，就是特殊性质的格如何构造顶点算子代数的过程。有了前面的经验，我觉得不要让ai迈的步子太大，就找出几个核心定理让它先证明，比如那个8.6.1和8.8.9的核心对易子式。我想着这样应该搞定起来不难了吧，确实ai也一次次地汇报了进度，一次次地看似在不断地推进，但这次是证明核心定理了，但是挣扎好几天以后，ai连8.6.1都证明不出来，我感觉到了不对劲。这时我才明白，我高估了ai的能力，也高估了写书者的能力。先说书吧，我以前确实也深入研究过，但太久远了，搞得我也有点陌生，但一点点找回记忆的过程中，我发现这本书可能并不适合ai，原因很简单，因为各种符号太分散了，一个小小的撇号或横线其实都有着特殊含义，但它分散在前面的各个地方，而且还出现符号含义的变更，我把它理解清楚都再一次花了好久的时间，至于ai呢，它的注意力机制让它很难把符号全部关联起来的，导致好几个地方都出现了脑补误读，这其实也是人容易放的错误。这就会导致证明过程中性质的缺少，完全不足以退出想要的定理，最后只能在似乎有效的化归中兜圈子。拿FLM定理8.6.1来说，第一眼看到a,b上横线的时候，确实很容易让人以为只是一个元素的特殊写法，你不仔细读全文就不会知道，这其实是一个格中心化子到格自身的同态。其实如果是我的写书风格，每个有歧义的符号绝不会放太远，一定要放到定理的附近，要么就是术语本身凝聚了符号的含义，这种风格其实更适合ai的注意机制。
别怕我还没放弃，于是我进入了下一个阶段，先陪着ai从下往上地把整个定义链条给梳理一遍，确保每个定义都是和书基本一致的，这样定理的前提应该就足够了，证明应该也不是什么难事了。然后就是sorry一次次的化归，虽然令人兴奋，但还是死活证明不出来，没有尽头。仔细阅读才发现，我之前不要弱化定理的思想钢印好像起作用了。化归为不弱化的命题是好事，但是你丢失了要证明的最后定理的很多性质，得到了一个极强的sorry命题，这稍微动点脑子都知道是证明不出来的。所以我又给ai加了一个驳斥机制，每次拆分sorry的时候，先用特例验证一下命题是否为假，假命题就不要推了，直觉往回撤。这是我感觉已经把方法论全部穷尽了，总能把定理证明出来了，然后呢？然后就变成了无止境的驳斥戏码……能不能不要让我这么无语？直到这时我突然开窍了，当前的llm通用ai似乎完全没有对lean4进行大型工程的训练，做点小模块确实还好，但很多基本的lean4证明思想都没有，还要我去教，甚至教了还做不好。哎，我也觉得很可悲，现在的大部分ai估计全都在卷编程之类的东西，所以做lean4形式化的时候，用的也基本是编程思想，想让ai完成这样一个大任务，估计只能寄托于那些lean4特化的模型或是a和o的内部大模型，对我们来说都遥不可及，或许唯一能干的就是，让llm通用ai辅助我们完成小模块的形式化，这方面ai表现的还可以，lean社区的大多数项目差不多也是这样，这样还能更好地把握进度加深理解，直接让ai自动化干一个大lean项目，目前有些困难，特化模型或许有些搞头，又或者是我没有玩明白工作流，反正钱是砸不动了。
钱确实可惜，啥实质内容也没干出来，但就当是花钱买了课程吧，因为这次以后我比以前更懂得lean4了。其实我觉得数学终于是好起来了，未来数学也变得更严谨了，其实以前一直有个老大难的问题，深入懂数学的人不懂lean，深入懂lean的人不一定懂数学，但ai来了它就是一个很好的翻译桥梁，像我这样的一般人就可以用自然语言去做数学理解数学，然后再让ai把它形式化严格化，如果发现漏洞，ai可以把lean翻译回来让我继续攻克，当然有时候ai可以自行修补所谓的显然。而且通过lean语言，ai可以更加严谨地向别人介绍数学。其实在我看来lean其实就应该是ai内部的严谨数学语言，然后我们人类用一套稍微不太严谨的自然语言数学，翻译桥梁的话，ai能做人也能做，这是一个很好的互惠范式。
Eine mathematische Theorie ist erst dann vollkommen, wenn man sie so erklären kann, dass sie der Mann auf der Straße versteht.我觉得ai正在做到这一点，数学与严谨终于开始属于每一个人了，这绝对是好事。