Sequencelib: A Computational Platform for Formalizing the OEIS in Lean

TL;DR

This paper introduces Sequencelib, a Lean-based platform that formalizes the OEIS, enabling automated theorem proving for over 25,000 sequences and 1.6 million theorems, enhancing mathematical knowledge management.

Contribution

The paper presents a novel formalization of OEIS sequences in Lean, including tools for metadata attachment and theorem derivation, and a scalable server for large-scale formalization.

Findings

Formalized over 25,000 OEIS sequences

Proved more than 1.6 million theorems about sequence values

Developed a transpiler translating Standard ML to Lean

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.