我觉得 AI 以后应该可以理解。现在的 LLM 还是不够大，上下文还是太短。再发展个三年，参数达到 1E params, 有效上下文能够达到 1T tokens 时，搞这些还是手拿把掐。

【 在 z16166 的大作中提到: 】
: Haskell的约束可能又过于严格了，AI的概率模型也可能搞不定其中复杂的那些。
: 陶哲轩在推动的Lean 4则更加严格
--
FROM 27.152.53.*