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).)
On Fri, Nov 29, 2024 at 2:11 PM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/6e91b35c-d43b-4d9d-a1cb-074846ba23edn%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/CAFXXJSusKB-NGOH0OU6vwhZgyonsAWFOq1HsHLP-6CZV%3DDj3WQ%40mail.gmail.com.
