加州理工团队解决了形式化研究神器Lean运行LLM推理时的核心技术挑战，可以让LLM在Lean中提出证明策略，允许人类以无缝的方式干预和修改。 Lean Copilot，让陶哲轩等众多数学家赞不绝口的这个形式化数学工具，又有超强进化了？ 就在刚刚，加州理工教授Anima Anandkumar宣布，团队发布了Lean Copilot论文的扩展版本，并且更新了代码库。 论文地址：http

数学家陶哲轩在Lean4形式化证明时发现已发表论文中的错误: 陶哲轩在用Lean4发现了一个小错误：论文论证中出现的表达式 12logn-1n-k-1 在 n=3,k=2 的情况下实际上是发散的。幸运的是，这个问题只影响到较小的 n 值，对于 n≥8 的情况，整体论证仍然成立，更小的 n 值可以用更粗糙的方法处理。陶哲轩将添加一个脚注，承认之前版本的论证略有错误，这是在 Lean 中通过形式化发

笔者通过观察黎曼积分相关定理、定义的结构，发现其和序列定义的相似性。于是最终成功构造出了一个和黎曼积分等价的序列-胡杰黎曼序列，通过该序列就能证明，黎曼积分的所有定理、性质、甚至是定理的证明，都可以被归约为序列极限相关的性质证明 本文编写于14日精读掌握《陶哲轩:实分析》,day12,2019/7.19