> 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 On Sat, Nov 23, 2024 at 7:51 PM Steven Nguyen <[email protected]> wrote: > 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/CAFXXJSuw%3DqOVc73TrvsYX1khkA9xB7pR1Kw0fDwP%3DNnFvjLT%2Bw%40mail.gmail.com.
