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
<http://set.mm>:
(1) Is set.mm <http://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
<http://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 <http://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 <http://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 <http://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>.
