LLM 开始替 Lean 写证明：形式化验证最贵的一步可能正在自动化

作者：林岚｜OC 开发者生态编辑