对 Lean4 的关键审视

Lean4 当前版本存在可被社区认定为漏洞的证明，例如 "True=False" 被接受的情况。Lean 社区已发现其内核中七处额外漏洞，并认为 AI 可能会利用这些漏洞生成不可靠的证书。文章指出，Lean4 作为新兴软件仍存在问题，对其证书的信任需谨慎评估。