数学小站

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

探索数学形式化的新工具，管理大型证明项目的得力助手

前文对 Lean 开发三件套工具(elan、lake 和 lean)进行了介绍，这些工具的组合类似于 Rust 的 rustup + cargo + rustc 或 Node.js 的 nvm + npm + node 等语言生态中的工具链。在介绍了 Lean 项目的基本结构和文件组织方式后，本文将通过实战演练，展示 Lean 项目的完整开发流程，包括项目创建、依赖管理与配置、元编程代码编写，以及测试、自动化和收录等环节。

REPL (Read-Eval-Print Loop) 是一个交互式编程环境，它允许用户输入命令，执行并看到结果。Lean 4 REPL 基于 JSON 通信的交互式环境，它支持三种工作模式。

学习 Lean 的途径很多，具体取决于你的背景和偏好，这些教程有偏重数学的也有偏重编程的。

在本地搭建 Kaggle 竞赛环境，以 AIMO 竞赛为例，环境配置、代码提交，以及使用 vLLM 运行 DeepSeek-7b 模型的示例。

我们从数学角度和形式化角度分析了 AlphaProof 的工作。模型技术角度也有许多值得深入研究的内容，如数据合成方式、策略空间的定义、以及采用的搜索算法等，这些我们在 IMO 后续系列中整理介绍。

数学形式化的目的是提供一个完全客观和可验证的证明过程，使得任何了解该形式体系的人都能够检查证明的正确性，而不需要对证明本身进行主观判断。由于数学形式化能用于消除模型幻觉，在当下格外受到关注。

探讨了 Numina 在第二届 AIMO 竞赛中的技术方案，包括模型微调和推理算法。在数据集方面，Numina 开源了多个数据集用于模型的微调和验证，开放了微调各阶段的模型参数。Numina 取得最佳成绩的关键因素在于其**高质量的合成数据集**，其次是精心设计的微调技术和推理策略的选择。

SciBench，一个基准套件，用于评估 LLMs 解决大学水平科学问题的能力。