There is a "SetMM" theory in proofgold that includes primitives for the basic set.mm terms. Two exceptional cases are wi (translated as implication in Proofgold) and wal (translated as universal quantification over the base type set in Proofgold). The contents below were derived from a version set.mm from 2022.
There is a special version of Megalodon supporting SetMM available here. When this Megalodon is given the -setmm option it will be able to parse, proofcheck and create Proofgold document files corresponding to the SetMM theory. It will also parse wi and wal as implication and universal quantification, even though they are never explicitly declared.
Four preamble files for Megalodon are available:
For the sake of the curious, a single file with all of set.mm in a Megalodon checkable format is available as setmmall.mg.
Megalodon can check this (in about 2 hours) as follows:
A single Proofgold document could be generated as follows:
However, this Proofgold document would be far too large to be published into the Proofgold block chain.
An html version could be generated as follows:
Each of the 40555 set.mm theorems is translated into a single .mg files with its proof.
The directory is available as setmmmg.tgz (45M, unzipping to about 600M). Using tar xzf this gives a directory with a README, the DefaultElts.mgs signature file, and 40555 .mg files.
One of them can be checked as follows:
An html version of the file can be created as follows:
A Proofgold version of the file can be created as follows:
General information about how to publish Proofgold documents is available here,
and specific information about publishing these SetMM documents is below.
This Proofgold document has already been published
and can be viewd on a Proofgold block explorer here.
While Megalodon can be used to create the pfg and html files,
they are also available to download as setmmpfg.tgz (58M, unzipping to 900M)
and setmmhtml.tgz (373M, unzipping to 9G).
Megalodon is not needed at all to create Proofgold documents.
It is simply a relatively user-friendly way to do it.
Proofgold documents are written as text files (usually with the suffix .pfg, though this is in no way enforced).
The text files are a sequence of document items (e.g., theorems with proofs)
with types, terms and Curry-Howard style proof terms written in a simple prefix notation,
described here.
If the text file is a document in the SetMM theory, it must begin with the line
identifying the SetMM theory.
The type Base 0 corresponds to the base type of sets.
MetaMath uses a base type of classes, but these are translated into
Proofgold as the function type from sets to proposition,
which in native Proofgold format is written TpArr Base 0 Prop.
The primitive terms Prim n with n between 0 and 1290
correspond to the SetMM primitives described above.
Proofgold will know the types of these primitives by looking up the SetMM theory.
It will also know everything previously proven can be imported as a Known
proposition, including the SetMM axioms.
It should be easy to modify a MetaMath0 checker to output this Proofgold format directly, bypassing Megalodon.
After one has a Proofgold document as a .pfg file (created by Megalodon or in any other way), the way to publish into Proofgold is using the Proofgold commands readdraft, addnonce, addpublisher, commitdraft and publishdraft. The procedure is as follows:
Proofgold documents may contain conjectures.
In the .pfg files these entries start with Conj instead of Thm
and do not contain a proof term.
In Megalodon, these are given as theorems with Admitted instead of a proof.
For example, consider the file mmset_idi.mg with contents:
If we copy this to a new file and replace the proof with Admitted we have:
We can then create the corresponding .pfg file using the -pfg option in Megalodon to obtain:
The first line simply identifies the file as a document in the SetMM theory in Proofgold.
The second line declares that the first base type will be called "set" (though this is not used here).
The last line is the conjecture.
A Proofgold file for a document with a conjecture can be published in Proofgold as outlined above. Before publishing it, the creator may (or may not) place a bounty on the conjecture.
For example, a 2 bar bounty could be placed on the conjecture idi
by adding the following line (to the 3 line file above):
The NoTimeout keyword indicates the bounty can only be claimed
by proving idi or its negation. If the user placing the bounty
wanted to be able to reclaim the bounty after some time (say, at Proofgold block 50,000)
without idi or its negation being proven, the line could be
where PfgAddress should be the user's Proofgold address.
Even before, or after, a document with a conjecture is published, bounties can be placed. All one needs is the address of the conjecture, and this will be reported by the readdraft command (even if the user never publishes the draft). With the address of the conjecture, the bounty can be placed using the sendtoaddress command in Proofgold.
Information about collecting bounties using is here. In brief, create a document with the proof of the conjecture (or its negation), publish the document as outlined about, and then use the collectbounties command in Proofgold