combinatorics

[Peter Dolland]

Hello Metamath Community,

I'm still new here. So let me explain my intention, what I want here. My
original motivation comes from combinatorics. I am interested in the
relationship between the specification of an algebraic structure (such
as directed or undirected graph, magma resp. groupoid, semigroup, group,
topological space, partition, etc.) and the sequence that indicates how
many non-isomorphic instances of the structure there are over a set with
n elements, where n=0,1,2,3,.... . These sequences are published on
oeis.org: A273, A88, A1329, A27851, A1, A1930, A41,... . For some of
them, a generating algorithm (in some programming language) is also
given. However, in none of these sequences is a formal specification of
the underlying algebraic structure given, although this is often much
simpler than the generating algorithm.

My impression so far is that the desired specifications can be created
with MetaMath without any effort, as long as they are not already
contained in set.mm. A real challenge would probably be to verify the
specified algorithms against the specifications. It seems to me that a
basis of theorems would have to be created first. In particular, Polya's
counting theorem would need to be formalised. But perhaps one of you
knows what already exists on this topic and can be used.

Irrespective of this, it also seems worthwhile to me to create a bridge
between MetaMath and OEIS in such a way that MetaMath specifications are
added to corresponding sequences. The aim here could be to improve the
findability of sequences. For example, the additional criterion that the
elements of the carrier set are to be regarded as different (labelled)
could be achieved by adding an independent complete order relation. For
example, compare the sequences A88 with A53763, A273 with A2416, A41
with A110 or A1930 with A798. So you can see the first sequence is for
each pair the unlabelled version. And the second ones yield the labelled
version.

I see a need for action that goes far beyond my areas of different
expertises. The question now arises as to whether there are people in
your community who are willing and able to support me in my search of a
bridge as mentioned above. I have to admit that I have not yet delved
very deeply into MetaMath and set.mm. If I find someone here, I really
will have chance in order to acquire the necessary knowledge and skills.
I am hopefully very convinced that MetaMath makes a decisive
contribution to the further development of mathematics and computer
science by formalising important statements.

With best wishes,
Peter Dolland

[Steven Nguyen]

As a current description, by default people work on their own often-overlapping
topics, with the help of the community answering any questions. I'm unsure so
I'll leave the question of contributors open.

The project proposed here seems highly interesting. I think the main part
of the work is simply defining all the functions, since many concepts haven't
been defined yet.

One potential difficulty is that Metamath currently does not have much tooling.
So computer-generated proofs are ironically tedious and manual to prove by
default (not sure if https://us.metamath.org/mpeuni/631prm.html was done
manually; https://us.metamath.org/mpeuni/ax-bgbltosilva.html is also illustrative).
Computer-generated proofs are rare in math, luckily. But if the plan is to prove a
very large amount of sequences then I imagine it would be more efficient to make
the tooling for it first. Or (dun dun dun?) ask the Lean community. Teamwork
makes the dream work, in this case the sequences are math-community-wide so
I'd imagine the larger amount of people doing Lean proofs would make it easier.

I don't see any other strategy than starting with some sequence, and start seeing
what needs to be done (a lot). As a start, here's A1, informally the
(number of groups of order N), the definition is
(number of groups of order N, mod equivalence)
a1 = ( n e. NN |-> ( # ` ( { g e. Grp | ( od ` g ) = n } /. ~=g ) ) )

[Mario Carneiro]

> not sure if https://us.metamath.org/mpeuni/631prm.html was done manually

It was not, I wrote a numeric evaluator tactic for mmj2 to produce those proofs. There is an old video about it: https://www.youtube.com/watch?v=PF9cL3RABIw

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/a333331f-693f-4d44-86c0-74f8c7a09611n%40googlegroups.com.

[Peter Dolland]

Thank you, Steven, for formalizing oeis-a1! I think, there will be a general counting function assigning to any extensible structure class 𝒞 and a given cardinality ק the cardinality of the quotient of the subclass of 𝒞 having carrier sets with cardinality ק . The restriction of this function to finite cardinalities will give the OEIS sequences.

But first I have a few questions about using Metamath and set.mm:

(1) Is set.mm (without proofs) available as pdf? The book describes how I can create LaTeX input for individual statements or proofs, but not how the entire structure, including the important introductory paragraphs, can be integrated. Cross references to definitions would be nice.

(2) Either is there another tool to get the definition of a symbol in a quick way? (also vim macros are welcome!)

(3) I would like to test your definition of a1. But I do not understand, how to do this without changing set.mm. There is no second read possible.

These are not the only questions I have when dealing with Metamath. But I hope that answering them will make it a little easier for me to get started.

[Alexander van der Vekens]

As for the prime numbers (see https://oeis.org/A000040), are you talking about an enumeration of the primes, like (p`n) = the nth prime number? We have the beginning of this sequence in set.mm, see ~2prm, ~3prm, ~5prm, ~7prm,

~ 11prm, ~ 13prm , ~17prm, ~19prm, ~ 23prm, ~37prm, ~43prm,  ~83prm, ~139prm, ~163prm, ~317prm, ~ 631prm, ~1259prm, ~2503prm, ~4001prm (which, of course, is not complete; e.g., ~29prm is missing).

I can imagine to formalize such a function (recursively), but it would be very difficult to evaluate it (for example to prove that (p`2024) = 17599) with Metamath.

[Mario Carneiro]

We have the prime pi function, which is the inverse of the nth prime function, but I don't think we have a definition for the nth prime function itself. (Having the definition can be useful even if you can't easily evaluate it efficiently, e.g. to prove asymptotics (https://us.metamath.org/mpeuni/pnt.html).)

To view this discussion visit https://groups.google.com/d/msgid/metamath/6e91b35c-d43b-4d9d-a1cb-074846ba23edn%40googlegroups.com.

[Steven Nguyen]

(1) No, the closest thing are the web pages: https://us.metamath.org/mpeuni/mmtheorems1.html.
https://metamath.tirix.org/mpests/selvcl has the feature where clicking on a symbol takes you to its definition. On the web pages the closest thing is clicking on a particular Syntax hint and then clicking the actual definition.

What you are describing sounds quite nice though. Though the file would probably be quite long so ideally such a tool could output just for a section.

(2) This is probably very possible: here's a multiline regex that matches definitions:

df-[\w.]+\s+\$a[^$]+\$\.

The symbols -> -. A. e. (and a few mathbox symbols) do not have a corresponding definition, but otherwise it should be possible to map symbols to definitions by seeing what definition is the first to use a symbol.

https://us.metamath.org/mpeuni/mmdefinitions.html exists too. It's rather large and shows all syntax and axioms too. If you're using metamath.exe you can do "search df-* symbol" which outputs all definitions with "symbol", and other tools have cooresponding search functions.

(3) (Cannot read a second file) You can make a new file that simply includes the file: "$[ set.mm $]" and read the new one. Example: https://github.com/icecream17/Stuff/blob/main/math/~w2.mm

[Igor Ieskov]

Hi Peter,

(2) Either is there another tool to get the definition of a symbol in a quick way?

You can use metamath-lamp tool to find definition of a symbol https://expln.github.io/lamp/latest/index.html When you load set.mm into it, you can open Explorer tab, then put “df-” to the “Label” field and press Enter. This will show a list of definitions (I am not sure if all the definitions will be shown, but I guess the majority of them will be). If you need the definition for some particular symbol, then instead of putting “df-” to the “Label”, put the symbol to the “Pattern” field and press Enter. This will show all assertions containing that symbol. Usually the definition of a symbol is located at the beginning the list. Also, if you use metamath-lamp to view proofs, and you want to see the definition of a symbol you encountered in a proof, you can click that symbol and then click the “Search” button which should appear under the statement you clicked. This will open a new Explorer tab showing all usages of that symbol, including its definition. Before clicking the search button, make sure that only the symbol is selected. If other surrounding symbols are selected too, then click the “Shrink selection” button, so only the symbol you are interested in becomes selected.

-

Igor

[Peter Dolland]

I didn't talk about the prime numbers. But if you have a (n extensible) structure whose counting sequence (for finite carriers) yields A40, I would very appreciate.

To view this discussion visit https://groups.google.com/d/msgid/metamath/6e91b35c-d43b-4d9d-a1cb-074846ba23edn%40googlegroups.com.

[Peter Dolland]

Steven, what do you think about

genCount = ( s e. _V |-> ( n e. NN |-> ( #  ( { e e. s | ( od  e ) = n } /. ~=g ) ) ) )

? So, we would have

a1 = ( genCount ` Grp )
a688 = ( genCount ` Abel )
a122 = ( genCount ` Poset )

etc.

To view this discussion visit https://groups.google.com/d/msgid/metamath/eefae3e0-4c54-4b6c-90cf-dc6269764b10%40gmx.de.

[Peter Dolland]

I think, we should use ~=c instead of ~=g. So we have the ismorphisms for any category.

[Peter Dolland]

I am beginning to understand that we need to define an isomorphism class for every extensible structure. But I think furthermore, that this could be done in a generalized way:

isoClass = ( s e. _V |-> ...? )

The corrected definition of genCount would then look like:

genCount = ( s e. _V |-> ( n e. NN |-> ( # ` ( { e e. s | ( od ` e ) = n } /. ( isoClass ` s ) ) ) ) )

Am 02.12.2024 um 21:46 schrieb Steven Nguyen:

reverse-chronological
(1) That's a great idea to generalize it. Though, for instance, rings being group-isomorphic does not imply the rings are ring-isomorphic: isrhm - Metamath Proof Explorer so it's imagine it's somewhat limited. I'm not very familiar with category theory so maybe I'm missing something.

(2) genCount (non-generalized) is another kind of generalization, again great idea. And corresponding to (1), the particular definition using ~=g could be named grpCount, genGrpCount, or #_grp (whichever feels most familiar)

(3) As for prime numbers we have df-ppi - Metamath Proof Explorer and we can verify what the nth prime number is by, say, ppi3 - Metamath Proof Explorer