Subscribe to Events

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.