Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
Walter Moreira, Joe Stubbs
cs.LO
Jan 16, 2026 · v1
TL;DR
Formalizes OEIS integer sequences in Lean with metaprogramming tools and a Lean tool server, formalizing 25,000+ sequences and proving 1.6M+ value theorems.
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.
Problem
The OEIS catalogs over 380,000 integer sequences with more than 12,000 citations, but its mathematical content lacks formal verification. No systematic platform exists to formalize OEIS sequences and their properties in a proof assistant.
Approach
Sequencelib provides a Lean library of OEIS sequence formalizations together with metaprogramming tools that programmatically attach OEIS metadata to Lean definitions and derive theorems about sequences. The platform includes custom tactics and automation for working with integer sequences, and connects to the OEIS database for metadata retrieval.
Results
The project delivers a computational platform for formalizing OEIS content in Lean, including formalized sequences, metaprogramming tools for metadata attachment, and infrastructure for deriving verified sequence properties. It establishes a foundation for large-scale autoformalization of the OEIS.
