COPRA 把 GPT-4 包装成可回溯 formal proof agent，确立 generate–execute–observe–revise 循环

COPRA 使用通用 GPT-4，而不是专门微调的 prover：agent 在 Lean / Coq 中提出 tactic、执行、读取 proof-state 与错误反馈、维护 search history 并在失败时回溯，同时可检索外部 lemma。论文报告其在 miniF2F 上显著优于 few-shot GPT-4，并在 pass@1 上超过当时的 ReProver；代码与数据公开。