数学小站

数学竞赛大致分为两类：一类面向高中生，例如国际数学奥林匹克竞赛（IMO）及相关选拔赛；另一类涵盖本科以上知识，如全国大学生数学竞赛和阿里巴巴数学竞赛等。IMO 作为高中生数学竞赛的巅峰赛事，由于背景知识需求相对较少，成为了测评 AI 能力的绝佳试金石。

由于 LLM 的幻觉问题，数学形式化——这一消除幻觉确保论证严谨性的手段——受到了很多关注。按照陶哲轩的说法，形式化是在前严谨阶段到严谨阶段的过渡，能避免常见错误和消除误区。然而，数学真正具有创造力和生命力的地方在于后严谨阶段。在这一阶段，研究者在已经掌握严谨理论基础的情况下，开始建立和形成数学直觉。如果 LLM 能够在后严谨阶段发挥其作用，那么它很有可能会真正引起数学学术界的广泛重视。

在数学研究领域，计算推导是不可或缺的一环。从上世纪 60 年代开始，数学家就开始使用计算机辅助发现模式和猜想。如今，专业的数学编程语言，如 Mathematica，Maple，SageMath，GAP4 等，应运而生，极大地拓展了人类的计算能力。这些语言使我们能够完成传统手算难以实现的任务。在 LLM 快速发展的时代，编程任务可以通过 AI 辅助更轻松地完成。我们将在无需自己编写代码的情况下，借助 LLMCoder 来辅助对问题的探索思考。

SageMath 简介，开发版的安装教程。

Lean 定理证明器的 Python 交互库，支持 Lean 3 和 Lean 4。

深入了解 Lean4Game 教程，学习如何开发游戏，构建丰富的互动学习体验。

唠唠闲话

安装配置

如果不方便配置环境，或者只是想快速了解这门语言，推荐使用在线服务，gitpod 或者 github-codespaces。

下边介绍本地运行方式，LEAN4 的安装可参考教程：「Lean 4 安装教程」。

此外，安装依赖的过程，需要下载 GitHub 资源，确保网络畅通。

下载仓库：

1

git clone https://github.com/Lean-zh/GlimpseOfLean.git

首次打开，需等待构建，如下图：

当然，也可以选择在命令行进行构建，使用 lake 包管理命令。

1
2

lake update # 更新依赖包
lake build # 构建依赖

构建阶段要编译 mathlib 库，通常要等待较长时间。

快速示例

我们仅介绍 GlimpseOfLean 的引用的例子。其他内容可以翻阅翻译的文档。此外，只有看是不够的，建议上手练习，一共就几个文件。

本次研讨会共 41 篇论文，这些工作基本包含了近期 AI 结合 Math 的主流方向。我们将文章按以下主题整理（类别间可能存在交叉）：1. 形式化 2. 研究导向 3. 数据集 4. 工具 & 智能体 5. 数学推理 & 应用题 6. 小模型实验 & 训练微调 7. 多模态 8. 认知科学。

OpenAI 发布了 GPTs，允许用户在 ChatGPT 上通过对话构建自己的 GPT。我第一时间也做了测试，并尝试了两个任务，构建 LEAN 形式定理生成器，以及增强 ChatTool 使用体验的工具。

Lean 是一个交互式定理证明器，也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。