OEIS

Stream: maths

[Amir Livne Bar-on]

In the same project we'll need this counting sequence too: https://oeis.org/A103293

I guess this is too esoteric to have been formalized.

[Kim Morrison]

Maybe someone needs to create https://github.com/leanprover-community/oeis

[Kevin Buzzard]

I could imagine that this would be a really fun project! The OEIS often contains code for sequences written in e.g. mathematica or pari. It would not surprise me at all if the OEIS folks were open to including Lean code, they have always seemed very liberal in what they would accept (in the past I've sent them pari code for sequences and it's just been uploaded with very little fuss). But making a lean repo where people just start defining functions corresponding to the sequences is something where a lot of people might consider joining in. It's certainly much easier than formalising IMO solutions!

[Damiano Testa]

Maybe, even AI formalizing some of the OEIS entries is feasible.

[Kevin Buzzard]

AI is already doing that -- @Josef Urban et al have a system which looks at an OEIS entry and attempts to autonomously write python code which reproduces it. I had a look at this paper and what they do is really quite surprising -- for some sequences it's dead easy, but there were others I found where the sequence had a complicated explanation, the python program was definitely not implementing the explanation and looked like a completely random piece of code written by a machine, but the code was outputting the sequence. See https://arxiv.org/abs/2301.11479 for more details. I found at least one example where the code was definitely wrong in the sense that if I generated more terms of the sequence then the python program would diverge from the answer, but it was also definitely right multiple times.

[Joseph Myers]

Since Lean code depends strongly on particular Lean and mathlib versions and needs updating frequently as those change, a Lean project with definitions of OEIS sequences seems much more useful than putting the code directly in OEIS and letting it bitrot quickly.

[Joseph Myers]

Note that Sean Irvine has Java code for over 150000 OEIS sequences - https://github.com/archmageirvine/joeis - and does automated validation that the terms calculated by those implementations match those on OEIS. For any kind of Lean definition providing some way to calculate or prove individual terms of a sequence, such validation seems important to have as well.

[Joseph Myers]

It's a lot less clear what it would mean to have a sequence defined in Lean than it is for those Java implementations. Any or all of the following are possible:

• A definition suitable for proving things about the sequence.
• A definition suitable for computing terms of the sequence (whether through direct execution of the Lean function, or through kernel reduction).
• Proofs that multiple such definitions do define the same sequence.
• A tactic / norm_num extension for proving the values of terms of the sequence.
• Ad hoc proofs of the values of specific terms (given a suitable definition).
• Proofs of lemmas giving properties of the sequence and relations to other sequences. https://oeis.org/A000110 (Bell numbers) has a lot of such properties under "Comments", "Formula" and "Crossrefs". Most sentences there correspond to lemmas that could be given formal proofs.

[Joseph Myers]

As usual, it would be important to put relevant material in mathlib not only in a separate repository. For example, the definition and basic properties of Bell numbers certainly belong in mathlib (and then OEIS.A000110 might be defined in a separate project in terms of the mathlib definition, and lemmas relating it to other sequences proved in terms of corresponding mathlib lemmas). But no doubt there are also plenty of more obscure sequences and facts in OEIS, much less likely to be of general use, where a separate repository is a natural home.

[Joseph Myers]

And mathlib material might be in greater generality than material in a separate repository. Looking at the "keyword:core" sequences in OEIS, for example, A000079 is the powers of 2; we certainly don't need a separate def for that in mathlib, the instance for ^ on natural numbers suffices (but various standard properties of powers of 2 probably belong in mathlib). A000796 is the decimal expansion of pi; we should have base-N expansions of real numbers in mathlib (including tactics to compute terms given bounds on those real numbers), and we already have pi, but there may not be anything worth saying about the combination of those two concepts in mathlib. Many thousands of OEIS sequences are given by linear recurrences (or more generally D-finite sequences); the theory of such sequences belongs in mathlib, but beyond a few important special cases such as Fibonacci, the individual such sequences probably don't (and in a separate project, they should be defined automatically in terms of data giving the recurrence coefficients rather than writing Lean definitions manually for each one).

[Joseph Myers]

Given the various different things that might or might not be provided for an individual sequence in Lean (including proofs of lots of individual assertions present in the sequence description in OEIS), tracking what is / isn't included in any Lean OEIS project would be a lot more complicated than a simple yes/no for each sequence. (And even when doing a yes/no there would be the issue of what interface works for looking at state for over 350000 sequences.)

[Notification Bot]

11 messages were moved here from #Is there code for X? > Bell numbers by Eric Wieser.

[Yaël Dillies]

Could we move this to #maths ?

[Eric Wieser]

Done. Note there is this old thread too

[Yaël Dillies]

Might be worth merging them

[Eric Wieser]

I'll let @Kevin Buzzard decide, since he started the other thread

[Kevin Buzzard]

Happy to merge them! Great to see some youngster already had this idea in 2020!