Sequencelib: a computational platform for formalizing OEIS sequences in Lean 4

[Walter Moreira]

Hi all! We are excited to announce the Sequencelib project (https://provables.org/sequencelib/), a computational platform for formalizing the mathematics contained within the OEIS in the Lean 4 interactive theorem prover (https://lean-lang.org/). 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. These tools have been bundled into a scalable server, OEIS-LT, which has been used to successfully formalize more than 25,000 sequences from the OEIS and prove more than 1.6 million theorems about their values. Moreover, with our collaborators, we are actively developing additional tools and formalizations.

We welcome contributions to Sequencelib! You can find more information about the project, including how to contribute, from the project website (https://provables.org/sequencelib/getting_started/contributing/) or the GitHub repository (https://github.com/provables/sequencelib/). Additionally, we have written an initial paper on Sequencelib, which is available from the arXiv here: https://arxiv.org/abs/2601.11757

And we also welcome any feedback and ideas for new directions, to make Sequencelib a useful resource for the OEIS community.

Cheers!
Walter and Joe

[Andrei Zabolotskii]

Hi Walter and Joe,

This is interesting, I like the idea of the project and most of the implementation. Thank you!

One thing that perhaps needs to be fixed is that you uncritically accept the formulas (programs) from the AAAI-23 paper "Learning program synthesis for integer sequences from scratch" when you didn't find an explicit counterexample. But they still can be wrong, or conjectural at best. For example:

* A001231, A003829, A005026, A013927, A105510 -- these sequences have keyword "more" (and sometimes "hard") in the OEIS, and there is no reason to expect that the AAAI-23 formulas for them are correct.

* A105062 -- the formula is almost surely incorrect; possibly it is actually a formula for A120(n-1). (Admittedly, the sequence itself is an uninteresting.)

* A003860 -- this sequence has keyword "full", so it should be undefined beyond the given terms.

* A193840 -- this sequence has keyword "dead", it makes sense to exclude such sequences completely.

Perhaps jOEIS can serve you as a more reliable source of programs for sequences?

Best regards,

Andrei

пятница, 23 января 2026 г. в 01:31:41 UTC, gwal...@gmail.com:

[Walter Moreira]

Hello Andrei.

Thank you so much for pointing out those issues. Based on your comments, we added a tagging system to Sequencelib that uses the tags from OEIS and some heuristics (e.g., sequences with OEIS tags "hard" and/or "more" and few known values, are tagged as "low confidence" in Sequencelib). On a next iteration we might even fully remove them, or rework some of them with a new definition. We also added your name to the acknowledgements page (please, let us know if you prefer otherwise).

And thank you for the reference to jOEIS. 

Best wishes,

Walter