Talks Thursday about formalizing the OEIS using Lean
Neil Sloane
To OEIS folks:
There are two talks this Thursday that might be important for the OEIS.
Here is the anouncement:
From: Ayush Khaitan
Sent: Monday, April 13, 2026 8:00 AM
Subject: Seminar [at Rutgers University] this week.
Here is the Zoom link exactly as it was given to me:
o
Here is the Zoom link:
https://rutgers.zoom.us/j/96753161671?pwd=SzV0OUsrUUpVT0FITVhoQ3doaWkwdz09Links to an external site.
Passcode: 142980
This week, the Rutgers AI and Math seminar is hosting Joe Stubbs (UT Austin) and Walter Moreira (Independent researcher).
Date: April 16, Thursday
Place: Rm# 005 in Hill
Time: 10 am - 12 noon (two talks instead of one).
Talk 1: Sequencelib: A Platform for Formalizing the OEIS
Abstract: The On-Line Encyclopedia of Integer Sequences (OEIS) is a web-accessible database cataloging interesting integer sequences and associated theorems. With more than 390,000 sequences and 12,000 citations, the OEIS is one of the most robust and highly cited resources in all of theoretical mathematics. The Sequencelib project provides an open-source computational platform to formalize the mathematics contained within the OEIS using the Lean programming language. With contributions made through a combination of hand-written formalizations, metaprogramming, and AI, Sequencelib currently contains formalizations for more than 25,000 sequences and over 1.6 million theorems about their values.
In this first of two talks, we will provide an introduction to the Sequencelib platform and describe its position within the Lean ecosystem, including its relationship to Mathlib, Lean's massive open-source library of formalized Mathematics. We will define precisely what is meant by "formalizing an OEIS sequence", and we will walk through the steps involved in a typical sequence formalization, showing how to use the primary Sequencelib facilities that support metadata collection and proof synthesis within the Lean interactive theorem prover. We will also discuss some of the interesting sequences that have been formalized in Sequencelib and survey some areas for future work and contributions.
Speaker: Walter Moreira, UT Austin
Bio: Dr. Walter Moreira is a mathematician and software engineer that has experience across a wide spectrum of disciplines. With a background in pure mathematics, he has worked at the Astronomy Department at the University of Texas at Austin, the Texas Advanced Computing Center, and Canon Nanotechnologies, among other places. He specializes in developing software containing strong theoretical foundations and using formal methods. He is currently working on the formalization of the On-Line Encyclopedia of Integer Sequences.
~~~~~
Talk 2: Automated Formalization of OEIS using the Sequencelib Platform
Abstract: In this second talk, we will provide an overview of the design and implementation of the metaprogramming capabilities in Sequencelib, including the OEIS attribute, which can be used to automatically attach OEIS sequence metadata to a Lean definition, and the oeis-tactic, which can be used to automatically prove theorems about the values of sequences. We also detail OEIS-LT, a lightweight, multi-threaded Lean tool server that bundles these capabilities into a scalable, machine-friendly API. Together, these tools support automated formalization and proof synthesis (AFPS) workflows, and as an example, we describe the design and implementation of a computational pipeline that built on the work of Gauthier, et al. and leveraged OEIS-LT to formalize more than 25,000 sequences from the OEIS. Finally, we describe how OEIS-LT will be included in a new AFPS toolchain we have started building with our collaborators called AIProver, and we present some preliminary results from its initial use on Sequencelib.
Speaker: Joe Stubbs, UT Austin
Bio: Dr. Joe Stubbs is a Research Scientist at the University of Texas at Austin and leads the Cloud and Interactive Computing (CIC) group at the Texas Advanced Computing Center (TACC). CIC researches, builds and maintains national-scale cloud computing platforms and distributed systems for advanced research computing. He is the PI of multiple NSF-funded projects, and he leads TACC’s involvement in the NSF-funded ICICLE AI Institute. He also teaches courses and mentors students in the Computational Engineering program within the Cockrell School of Engineering at the University of Texas at Austin. His research and teaching focus on software engineering, scalable distributed systems design, formal methods and AI, and with Walter Moreira, he leads the Sequencelib project, a platform for formalizing the mathematics contained within the On-line Encyclopedia of Integer Sequences (OEIS) in the Lean 4 theorem prover.