Zulip Chat Archive

Stream: maths

Topic: OEIS Lean entries


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 29 2020 at 14:21):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:37):

Oh :)

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 14:37):

It's not in mathlib though :-(

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 14:38):

unless someone put it in

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 14:40):

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

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:40):

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

view this post on Zulip Mario Carneiro (Sep 29 2020 at 14:40):

enat

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:41):

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

view this post on Zulip Mario Carneiro (Sep 29 2020 at 14:41):

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

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:41):

Oh right.

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:41):

Sorry, I still think like a mathematician :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:44):

Yeah, I guess that makes sense.

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 14:44):

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

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 14:44):

and ideals of Z are canonically nat shrug

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 14:45):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 14:50):

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

view this post on Zulip Adam Topaz (Sep 29 2020 at 14:51):

Oh I see what you mean.

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 14:51):

but take the quotient and I think it's fine

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:00):

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

view this post on Zulip Adam Topaz (Sep 29 2020 at 15:00):

Am I being stupid?

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 15:00):

no because the groups will have automorphisms

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 15:01):

this is the map from multiplication tables to groups

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 29 2020 at 15:04):

Some centralizer of multiplication in S_n

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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