(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. [image: Screenshot 2024-11-29 090741.png] 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 On Friday, November 29, 2024 at 6:39:05 AM UTC-6 Peter Dolland wrote: > 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/16b8348f-310a-489b-a180-67a53c86bcfcn%40googlegroups.com.
