Conjecturing–Proving Loop 让 LLM 在 Lean 中递归生成并证明新猜想，开始从 solver 向 theorem-discovery loop 过渡

Kasaura 等人提出 Conjecturing–Proving Loop：LLM 生成新的 Lean 4 conjectures、尝试证明，再把已生成 theorem 与 proof 放回上下文，继续提出更复杂的后续猜想。作者报告该 pipeline 重新发现了过去数学论文中尚未 formalize 的 theorem；至少有一个 theorem 在缺少前序 in-context proofs 时，模型甚至在自然语言中也无法证明。