The On-Line Encyclopedia of Integer Sequences (OEIS) is a web-accessible database cataloging interesting integer sequences and associated theorems. With more than 12,000 citations, the OEIS is one of the most highly cited resources in all of theoretical mathematics. In this paper, we present Sequencelib, a project to formalize the mathematics contained within the OEIS using the Lean programming language. Sequencelib includes a library of Lean formalizations of OEIS sequences as well as metaprogramming tools for programmatically attaching OEIS metadata to Lean definitions and deriving theorems about their values. Further, we describe OEIS-LT, a highly scalable Lean server that exposes these tools via a low-latency API. Finally, using OEIS-LT and prior work of Gauthier, et al., we describe a computational pipeline that formalized more than 25,000 sequences from the OEIS and proved more than 1.6 million theorems about their values. Our method makes use of a transpiler, available in OEIS-LT, that is capable of translating a subset of Standard ML to Lean, together with a set of performance improvement transformations and proofs of correctness.

翻译：在线整数序列百科全书（OEIS）是一个可通过网络访问的数据库，收录了各类有趣的整数序列及相关定理。作为理论数学领域引用率最高的资源之一，OEIS的引用次数已超过12,000次。本文介绍Sequencelib项目，该项目旨在使用Lean编程语言对OEIS中包含的数学内容进行形式化。Sequencelib包含一个OEIS序列的Lean形式化库，以及用于将OEIS元数据以编程方式关联到Lean定义并推导其数值定理的元编程工具。此外，我们描述了OEIS-LT——一个高可扩展的Lean服务器，通过低延迟API提供这些工具。最后，基于OEIS-LT及Gauthier等人的前期工作，我们构建了一个计算流水线，实现了对OEIS中超过25,000个序列的形式化，并证明了超过160万条关于其数值的定理。该方法利用了OEIS-LT中提供的转译器（可将标准ML的子集转换为Lean），结合一系列性能优化转换与正确性证明。