Hello World!

哈喽，欢迎来到 lookeng.cn，博客定位是与数学关联的一切一切，这里是置顶博客，整理已写博文和计划展开的话题，欢迎交流~

数学 & 编程

21 年开始写博客(wzhecnu.cn)，个人签名是 Math + Computer = ?，用编程推进数学研究一直是我的兴趣。

研二暑假，因为这篇推送LEAN 计算机验证了解到了形式化证明领域，加上对 AI 指引的数学直觉的兴趣，博士转系计算机，开始探索 Programming for Math 的新思路。

去年年底 ChatGPT 发布，也激起了我极大的兴趣。我希望它能足够的智能，但当时它做简单的乘法都会出问题，而且很难直接用 prompt “教会”它。我希望能在向内（模型能力）和向外（应用构建）两个方面拓展它的能力，构建一个对数学研究真正有效的智能体。

---

博客计划

形式化 & 代数编程 & 论文阅读

形式化：

• 「LeanDojo | 为 Lean 定理证明器搭建桥梁」
• 「数学形式化 | Lean4Game 教程」
• 「Lean 4 安装教程」
• 「Lean & GPT | 构建自己的 GPT」
• 「NeurIPS 论文粗读」

竞赛相关：

• 「AI 改写数学竞赛 | 从 IMO Grand 到 AlphaProof」
• 「OpenAI-o1 分析实测 | IMO2024 第一题」

其他：

• 「华罗庚诞辰 113 周年」
• 「哥德巴赫猜想 x AICoder

---

近期计划

1. 陶哲轩在 IMO2024 上的演讲。
2. Program Aided Math research 相关工作的调研。
3. 数学竞赛数据集，Research Level 数据集的调研。
4. Lean 工具相关的工作，比如 LeanCopilot，LeanDojo，LeanGames，LLMStep，LLMLean