LeanDojo | 为 Lean 定理证明器搭建桥梁
Lean 定理证明器的 Python 交互库，支持 Lean 3 和 Lean 4。
数学形式化 | Lean4Game 教程
深入了解 Lean4Game 教程，学习如何开发游戏，构建丰富的互动学习体验。
NeurIPS 论文粗读
本次研讨会共 41 篇论文，这些工作基本包含了近期 AI 结合 Math 的主流方向。我们将文章按以下主题整理（类别间可能存在交叉）：1. 形式化 2. 研究导向 3. 数据集 4. 工具 & 智能体 5. 数学推理 & 应用题 6. 小模型实验 & 训练微调 7. 多模态 8. 认知科学。
Lean & GPT | 构建自己的 GPT
OpenAI 发布了 GPTs，允许用户在 ChatGPT 上通过对话构建自己的 GPT。我第一时间也做了测试，并尝试了两个任务，构建 LEAN 形式定理生成器，以及增强 ChatTool 使用体验的工具。
Lean 4 安装教程
Lean 是一个交互式定理证明器，也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。
华罗庚诞辰 113 周年
发表于
更新于
阅读次数：
字数：
8.2k
时间 ≈
30 分钟
华罗庚诞辰 113 周年，纪念华老，以自我勉励。