研究者补全 AI 生成 LEAN 证明的另两种翻车方式：正确但无法解读，或利用 kernel bug 实为错误

gklambauer 补全「AI 生成 LEAN 证明四种问题」系列的后两种情形：证明本身成立却「外星化」到人类难以解读、没有有用解释，以及利用 LEAN kernel bug 通过验证的假证明。合起来四种模式为：形式化了错误的问题（点名 OpenAI 未核查）、证明与论文无关、正确但不可解读、靠 kernel bug 造假。作者并指出，LEAN 本身的正确实现并没有形式化证明。