## Stream: maths

### Topic: OEIS Lean entries

#### Kevin Buzzard (Sep 29 2020 at 14:07):

I've added things to the OEIS (link) before. Anything sensible gets accepted. I've certainly written code in pari-gp to compute some of the sequences and occasionally if I notice that a sequence doesn't have a pari-gp implementation I might add it, or at the very least put it on my infinitely long job list.

Now we have good summation convention I think it would look pretty neat if people started uploading Lean formalisations of the functions generating some of these sequences, especially some of the cooler ones like Ramanujan Tau (I should ask my contacts which pages get the most hits :-) ). Does this sound like a crazy idea? They certainly support plenty of other languages.

#### Reid Barton (Sep 29 2020 at 14:21):

It sounds like you're talking about generating functions, but it might also be interesting to just have Lean definitions of the sequences themselves, even if they're not computable in any particular sense.

#### Reid Barton (Sep 29 2020 at 14:21):

Can we do https://oeis.org/A000001 yet?

#### Reid Barton (Sep 29 2020 at 14:22):

A concern would be that mathlib is not really stable enough for a model where we submit a bunch of stuff to OEIS and then every so often some fraction of it breaks.

#### Kevin Buzzard (Sep 29 2020 at 14:24):

After Lean 3 development stops (and I'm assumimg it will at some point) there will be some canonical "Lean 3 mathlib" I guess; perhaps that would be a good target for stuff like this

#### Kevin Buzzard (Sep 29 2020 at 14:29):

Reid this one is easy: you take the category of groups, you look at the subtype of groups of order n, quotient out by the relationship generated by "we are isomorphic", and take the fincard.

#### Adam Topaz (Sep 29 2020 at 14:37):

Kevin Buzzard said:

Reid this one is easy: you take the category of groups, you look at the subtype of groups of order n, quotient out by the relationship generated by "we are isomorphic", and take the fincard.

Does mathlib know that this quotient is a finite type?

#### Kevin Buzzard (Sep 29 2020 at 14:37):

almost certainly not, but fincard just returns 0 if the type is infinite. It's noncomputable cardinality.

Oh :)

#### Kevin Buzzard (Sep 29 2020 at 14:37):

It's not in mathlib though :-(

#### Kevin Buzzard (Sep 29 2020 at 14:38):

unless someone put it in

#### Kevin Buzzard (Sep 29 2020 at 14:38):

I was working on a PR and then Chris Hughes sent me the xkcd about n+1 competing standards and it really put me off :-)

#### Kevin Buzzard (Sep 29 2020 at 14:40):

https://github.com/leanprover-community/mathlib/tree/fincard

#### Adam Topaz (Sep 29 2020 at 14:40):

Isn't there some standard type for $\mathbf{N} \cup \{\infty\}$?

#### Mario Carneiro (Sep 29 2020 at 14:40):

enat

#### Adam Topaz (Sep 29 2020 at 14:41):

So why not make the cardinality of an infinite type $\infty$?

#### Mario Carneiro (Sep 29 2020 at 14:41):

because it's annoying to not have a nat when you know it's finite

Oh right.

#### Adam Topaz (Sep 29 2020 at 14:41):

Sorry, I still think like a mathematician :)

#### Kevin Buzzard (Sep 29 2020 at 14:43):

fincard was really great for us. We used it to prove Sylow's theorem for a new definition of group, and @Jason KY. pushed the stuff we'd used to that branch but then the summer ended and now we're both busy with other things.

#### Kevin Buzzard (Sep 29 2020 at 14:43):

But for groups, the cardinality of a group is 0 iff the group is infinite, which is kind of cool

#### Kevin Buzzard (Sep 29 2020 at 14:44):

Same for the order of an element -- it was 0 if it was infinite. Turned out to be a really cool way to think about it.

#### Adam Topaz (Sep 29 2020 at 14:44):

Yeah, I guess that makes sense.

#### Kevin Buzzard (Sep 29 2020 at 14:44):

it's the kernel of the map from Z to G

#### Kevin Buzzard (Sep 29 2020 at 14:44):

and ideals of Z are canonically nat shrug

#### Kevin Buzzard (Sep 29 2020 at 14:45):

the multiplicative structures match up perfectly but the additive ones are completely destroyed

#### Kevin Buzzard (Sep 29 2020 at 14:46):

that's why I'm so grateful to people like @Aaron Anderson who have been removing additive assumptions from statements which are really about divisibility in monoids-with-zero. Johan discovered the objects, but we're still making the API in some sense. We've made great strides recently.

#### Kevin Buzzard (Sep 29 2020 at 14:49):

Oh how about this: type group (fin n) provably finite (hopefully by automation) and then simply put the isomorphism equivalence relation on that and then maybe you can even take the card.

#### Kevin Buzzard (Sep 29 2020 at 14:49):

I usually get stuck with the automation of finiteness and then have to ask @Chris Hughes to make it work :-)

#### Adam Topaz (Sep 29 2020 at 14:50):

You don't even need th equivalence relation. Just define the number to be the size of group (fin n).

#### Kevin Buzzard (Sep 29 2020 at 14:50):

I don't see why isomorphic terms would be equal though

#### Adam Topaz (Sep 29 2020 at 14:51):

Oh I see what you mean.

#### Kevin Buzzard (Sep 29 2020 at 14:51):

but take the quotient and I think it's fine

#### Adam Topaz (Sep 29 2020 at 15:00):

Isn't it enough to take the size of group (fin n) and divide by $n!$?

#### Adam Topaz (Sep 29 2020 at 15:00):

Am I being stupid?

#### Kevin Buzzard (Sep 29 2020 at 15:00):

no because the groups will have automorphisms

#### Kevin Buzzard (Sep 29 2020 at 15:01):

this is the map from multiplication tables to groups

#### Kevin Buzzard (Sep 29 2020 at 15:01):

but if you suddenly decide to switch elements b and c, some multiplciation tables changed but some didn't. The S_n action isn't free.

#### Kevin Buzzard (Sep 29 2020 at 15:03):

What you said is some kind of normalised groupoid total which counts groups up to some kind of weights related to the number of permutations of fin n which fix the group

#### Kevin Buzzard (Sep 29 2020 at 15:04):

Some centralizer of multiplication in S_n

#### Adam Topaz (Sep 29 2020 at 15:07):

Yeah I'm being stupid. I guess I never really seriously thought about what it means to "count the number of groups of order n".

#### Reid Barton (Sep 29 2020 at 17:02):

Anyways, it might be a nice project to try to collect Lean definitions of, say, the sequences listed in https://oeis.org/wiki/Index_to_OEIS:_Section_Cor#core.
It seems like the sort of thing people who are interested in concept alignment or specification of the contents of mathematical databases would find useful.

#### Joseph Myers (Sep 30 2020 at 00:26):

Sean Irvine has implemented 90000 OEIS sequences in Java. It might take a while to get that far in Lean, even if you only want definitions with no useful computational properties and no useful results about those definitions proved. (And really, if you define, say, the Catalan numbers, you probably ought to prove a few different things that definition counts, if not the very long list from Stanley's Enumerative Combinatorics.)

Last updated: May 12 2021 at 07:17 UTC