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 -- 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 [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/6bc5c9e0-2990-411a-b943-e41bcbb75b13%40gmx.de.
