LeanSide：自然语言证明的形式化协同推理系统

LeanSide 是一个形式化协同推理系统，允许用户以自由自然语言编写和修订证明，后端自动将其形式化为 Lean 并返回可理解的验证反馈。研究通过本科数学课堂部署的用户实验，分析了系统哪些特性帮助学生推进、哪些导致卡壳，并据此得出形式化后端在人机协同推理中的设计启示。