#用中间层链接人与计算机

AI4Math 的问题是，AI 直接写 lean4 代码，人看不懂；直接写自然语言（包括用自然语言推理），可能出现幻觉，需要大量智能体不断审核。而且即使 convience 了人类，也可能出错。

人类难以理解，这可能是因为

• 模型本身也不理解这个证明，仅仅是找到了它。
• 模型能够有某种理解，但是模型的写作能力太差。

另一个困难是难以验证正确性，需要转写成 lean 。但是这个转写过程是否确实正确，lean 代码是否可能证明了一个正确的但偏移、失真版本的结论？动辄百万行的 lean 代码没有任何可读性。

一方面，需要让结果能被人理解；另一方面，要能翻译到形式化验证。

##作为代码的论文

其实过去人类文章也很难读，不知道思路从何而来，各个定理关系是什么。
由于有一些 C 语言基础，所以我会用 C 的代码思路来读文章。将需要证明的主定理视作 main() 函数，其他引理等是被引用的函数。 现在有很多论文本身就是这个风格写作：先在 Introduction 章节声明主定理，在靠前的部分声明定义、记号等（#define），文章主体是引理、命题，在结尾 Proof of Main Theorem 的章节很短，往往是把前面的命题组装起来得到结论。 比较大的区别大概是 reference 放在结尾，而不是像 #include xxx 一样放在开头。

一个命题是形如 $A \implies B$ 的格式，把它看作函数，有输入和输出（都是statement），这个结构就像 C 语言的函数，对输入的格式有要求，函数本身的输出也有要求。

##伪代码

计算机领域有一条名言：没有什么问题是加一个中间层解决不了的，如果有，就再加一条。

加一个中间层，一个伪代码风格的，更简单直接的内容。

它应该是一种协议，一个定理/引理/命题的格式，但是并非代码格式，要更宽松一些。 能更好地被人以自然语言风格理解，这同样意味着能被 LLM 思考。
另一方面，这个伪代码应该有严格的部分，使得它依然可以有 lsp ast，来初步保证正确性。

##实现层面

这个目标可以在多个层次去尝试。

最底层的，我们可以直接修改模型架构，制造数学专用模型。参考多模态模型，或者 VLA 和 JPEA 模型那样，直接把输出部分的 token 限制为 lean 和这个伪代码/语言，并且让两个强绑定。
另外就是在 agent 和 harness 层面，设计一个伪代码的 prompt，让模型输出这个伪代码，并且在这个伪代码上做一些验证。

另一个模型层面的修改，是考虑 dllm 扩散语言模型，或者以这个思路为中心的非自回归的文本生成方式。具体见另一个想法。