OEIS Lean entries

Stream: maths

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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]

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]

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]

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]

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

[Adam Topaz]

Oh :)

[Kevin Buzzard]

It's not in mathlib though :-(

[Kevin Buzzard]

unless someone put it in

[Kevin Buzzard]

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]

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

[Adam Topaz]

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

[Mario Carneiro]

enat

[Adam Topaz]

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

[Mario Carneiro]

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

[Adam Topaz]

Oh right.

[Adam Topaz]

Sorry, I still think like a mathematician :)

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

Yeah, I guess that makes sense.

[Kevin Buzzard]

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

[Kevin Buzzard]

and ideals of Z are canonically nat shrug

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

Oh I see what you mean.

[Kevin Buzzard]

but take the quotient and I think it's fine

[Adam Topaz]

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

[Adam Topaz]

Am I being stupid?

[Kevin Buzzard]

no because the groups will have automorphisms

[Kevin Buzzard]

this is the map from multiplication tables to groups

[Kevin Buzzard]

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]

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]

Some centralizer of multiplication in S_n

[Adam Topaz]

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]

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]

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.)