用 Lean 形式化《From Linearity to Borrowing》，几乎全部由 Claude 完成

有人用 Lean 完整形式化了论文《From Linearity to Borrowing》，覆盖论文与技术补充材料中几乎所有定义和引理，包括 Fundamental Property 和 Adequacy（良类型程序最终以空堆终止）。这项工作几乎全部由 Claude 在 3-4 周内完成，作者与论文原作者无关，属业余学习项目。