#Between Natural Language and Codes

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

AI4Math 的问题是，AI 直接写 lean4 代码，人看不懂；直接写自然语言（包括用自然语言推理），太多幻觉，即使 convience 了人类，也可能出错。 一方面，需要让结果能被人理解；另一方面，要能翻译到形式化验证。

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

它应该是一种协议，一个定理/引理/命题的格式，但是并非代码格式，要更宽松一些。 能更好地被人以自然语言风格理解，这同样意味着能被 LLM 思考。
另一方面，这个伪代码应该有严格的部分，使得它依然可以有 lsp treesitter，来初步保证正确性。 一个命题是形如 $A \implies B$ 的格式，把它看作函数，有输入和输出（都是statement），这个结构就像 C 语言的函数，对输入的格式有要求，函数本身的输出也有要求。