Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
Walter Moreira, Joe Stubbs
TL;DR
Sequencelib introduces a Lean 4-based platform to formalize OEIS content, addressing ambiguities and correctness in sequence metadata by delivering a reusable library, metadata-driven metaprogramming, and a scalable API server. The system integrates a transpiler from a subset of Standard ML to Lean, a documentation-generation pipeline, and the OEIS-LT server to support AI-assisted formalization and programmatic access. A scalable pipeline built on these components formalized more than 25,000 OEIS sequence definitions and proved over 1.6 million theorems, demonstrating substantial throughput and practical viability as a benchmark for theorem provers and AI tools. The work highlights a path toward robust, machine-checkable representations of mathematical databases and provides infrastructure to study dependencies across sequences while enabling automated formalization workflows.
Abstract
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.