lean4oeis

LOEIS 是一个用于形式化 OEIS（在线整数序列百科全书）中整数序列的数据集，采用 Lean 4 和 Mathlib 库。该数据集包含从 OEIS 原始数据（约 398,471 个 .seq 文件）解析得到的元数据库（SQLite 格式，约 360 MB），以及基于此生成的 Lean 骨架代码文件（每个序列对应 LOEIS/<bucket>/<name>/{Defs,Data}.lean，初始含占位符 sorry）。数据规模在 10 万到 100 万之间，标签为数学、形式化验证、Lean、序列形式化。适用于数学形式化验证、定理证明辅助和自动推理研究。LOEIS is a dataset for formalizing integer sequences from the OEIS (Online Encyclopedia of Integer Sequences), using Lean 4 and the Mathlib library. It contains a metadata database (SQLite format, about 360 MB) parsed from the original OEIS data (approximately 398,471 .seq files), and Lean skeleton code files generated from it (each sequence corresponds to LOEIS/<bucket>/<name>/{Defs,Data}.lean, initially containing placeholder sorries). The data scale is between 100,000 and 1,000,000, with tags including mathematics, formal verification, Lean, and sequence formalization. It is suitable for research in mathematical formalization, theorem proving assistance, and automated reasoning.

原始信息汇总

LOEIS - Lean OEIS 形式化数据集

数据集概览

LOEIS（Lean OEIS Formalization）是一个专注于将 OEIS（在线整数序列百科全书）中的数学序列在 Lean 4 证明助手及 Mathlib 数学库中进行形式化验证的数据集。

基本信息

• 语言：代码（Lean 4）
• 许可证：CC-BY-SA-4.0
• 数据规模：100K 至 1M 条记录
• 数据来源：OEIS（在线整数序列百科全书）
• 标签：数学、形式化验证、Lean、OEIS、序列形式化

数据集内容

该数据集包含以下主要组成部分：

• Lean 源文件：为每个 OEIS 序列生成的 Lean 定义和数据结构
• 元数据数据库：Metadata/oeis.db（SQLite 格式，约 360 MB），存储所有序列的解析元数据
• OEIS 原始数据：从 OEIS 数据仓库获取的序列文件（约 1.6 GB，包含 398,471 个文件）
• 预构建缓存：cache/loeis-build.tar.zst 预编译产物，避免用户自行编译

工作流程

数据集提供了完整的流水线：

1. 元数据构建：通过 oeis-ingest 工具解析所有 .seq 文件生成 SQLite 数据库
2. Lean 骨架生成：使用 oeis-gen 工具从元数据数据库生成 Lean 定义文件（初始状态包含 sorry 占位符）
3. 编译验证：使用 lake build 编译所有生成的序列文件及聚合器

关键特性

• 支持按桶（bucket）、特定序列或全部序列进行定向生成
• 提供增量生成保护，避免覆盖已完成的证明
• 包含磁盘优化方案（如修剪 *.setup.json 文件，峰值磁盘占用从 ~1.5 TB 降至 ~100 GB）
• 提供预构建缓存恢复功能，支持快速搭建环境

使用说明

数据集提供两种使用方式：

1. 完整构建：从零开始构建元数据数据库并生成 Lean 文件
2. 快速恢复：直接下载预构建缓存，跳过编译过程

数据集当前状态处于公式形式化步骤之前，生成的 Lean 文件中仍包含 sorry 占位符等待后续填充。

搜集汇总

数据集介绍

构建方式

该数据集基于数学领域著名的OEIS（整数序列在线百科全书）构建，利用Lean 4及其数学库Mathlib对OEIS中的序列进行形式化验证。构建过程分为多个阶段：首先通过稀疏克隆OEIS的seq数据，并解析所有.seq文件，构建包含元数据的SQLite数据库；随后依据该数据库生成每个序列的Lean骨架文件，这些文件包含定义和数据，但初始用sorry占位；最后通过Lean构建系统编译所有生成的文件，确保每个序列的声明被验证。整个流程支持分批处理，并通过缓存机制优化构建效率。

特点

该数据集是首个大规模将OEIS序列形式化的尝试，包含超过10万个序列，每个序列都有对应的Lean定义和验证状态。其特点在于将抽象数学序列转化为可机器验证的形式，并提供了详细的元数据，便于检索和分析。数据集的构建采用自动化流程，支持分批生成和增量更新，且通过预构建缓存，用户无需从头编译即可使用。此外，数据集的设计文档（SPEC.md）和项目状态（AGENTS.md）提供了清晰的扩展指导，使其成为一个可扩展、可维护的形式化数学知识库。

使用方法

使用该数据集前，需安装Lean 4和elan，并获取Mathlib的预编译缓存。通过Git LFS拉取元数据库，或手动下载。用户可运行命令生成指定序列的Lean文件，或利用预构建的缓存跳过编译。数据集提供了丰富的命令行工具（如oeis-gen、oeis-cache），支持按桶或特定序列进行操作，并能管理构建磁盘占用。对于研究者，可基于生成的骨架文件补充证明，或将数据集集成至Lean项目中进行验证和进一步的形式化工作。

背景与挑战

背景概述

LOEIS数据集由formalica团队于2024年创建，旨在将整数序列在线百科全书（OEIS）中的数列形式化为Lean 4定理证明器与Mathlib库中的数学陈述。该数据集包含超过10万个序列，核心研究问题在于如何自动将数学序列的定义和性质转化为可验证的计算机证明，从而推动形式化数学与自动定理证明的发展。该数据集为数学与人工智能交叉领域提供了大规模基准，对验证数学知识库的自动化构建及数学推理的机械化具有重要意义。

当前挑战

领域层面，挑战在于将非形式化的数学序列描述转化为逻辑严谨的Lean 4定义，处理序列间复杂的依赖关系及数学概念的多样性，同时保持证明的可靠性与效率。构建过程中，面临数据规模庞大（原始数据约1.6GB，含近40万个文件）带来的存储与处理难题，以及需要自动生成可编译的Lean代码、管理约360MB的元数据数据库和高达1.5TB的构建体积等工程挑战，需设计缓存与增量构建机制以保障可行性。

常用场景

经典使用场景

lean4oeis数据集的核心场景在于为整数序列在线百科全书（OEIS）中的海量数列提供形式化的数学定义与证明。该数据集利用Lean 4定理证明器及其数学库Mathlib，将OEIS中每个序列的初始项和递推关系转化为可验证的定理陈述，并生成对应的Lean源码骨架。研究者可借此训练机器学习模型自动完成从自然语言数列描述到形式化证明的转换，或开发工具辅助数学家进行定理证明与序列性质探索，从而推动形式化数学的规模化发展。

衍生相关工作

围绕lean4oeis，已衍生出多个值得关注的研究方向。其生成的Lean骨架为后续的证明自动化算法提供了标准测试床，相关论文探讨了基于强化学习的策略优化在数列证明中的有效性。数据集提供的OEIS元数据与Lean形式化之间的映射关系，也启发了跨语言数学知识对齐的研究，例如将自然语言定理与形式化仓库进行语义链接。此外，其构建流程中的高效缓存与稀疏提取技术，为大规模形式化项目的基础设施设计提供了可复用的范例。

数据集最近研究

最新研究方向

LOEIS数据集聚焦于利用Lean 4交互式定理证明器对OEIS整数序列进行形式化验证，是数学与形式化验证交叉领域的前沿探索。该工作通过自动生成Lean骨架并逐步填充证明，旨在构建一个大规模、可机器验证的数学知识库，为自动定理证明、数学推理的机器校验以及AI辅助数学研究提供坚实数据基础。其研究意义不仅在于提升数学证明的可靠性，更在于推动形式化数学与机器学习在数学发现中的深度融合，为可解释、可验证的AI数学助手铺平道路。