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. Peter Dolland schrieb am Freitag, 29. November 2024 um 13:39:05 UTC+1: > 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. > > Am 23.11.2024 um 19:51 schrieb 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 ) ) ) > On Thursday, November 21, 2024 at 10:54:30 AM UTC-6 Peter Dolland wrote: > >> 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/a333331f-693f-4d44-86c0-74f8c7a09611n%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/a333331f-693f-4d44-86c0-74f8c7a09611n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- 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/6e91b35c-d43b-4d9d-a1cb-074846ba23edn%40googlegroups.com.
