GenLimitLib 用 Lean 4 对 language generation in the limit 文献做跨论文形式化，并面向 AI-assisted mathematics

GenLimitLib 在 9 月 29 日提交预印本，围绕由 Kleinberg 与 Mullainathan 引出的 language generation in the limit 理论构建 source-aligned Lean 4 library。作者报告 formal developments 覆盖 30 篇论文，并抽取共享定义、可复用证明组件和跨论文关系，同时通过数学案例与 LLM 实验讨论其对 paper understanding、conjecture generation、theorem proving 与 paper-to-Lean 的支持。