Wikidata:Property proposal/Metamath statement label

‎Metamath statement ID

Originally proposed at Wikidata:Property proposal/Authority control

Done: Metamath statement ID (P12888) (Talk and documentation)

Description	unique identifier for a theorem, axiom or definition in the Metamath set.mm database
Represents	Metamath (Q6822975)
Data type	External identifier
Domain	item, mathematical object (Q246672), mathematical concept (Q24034552)
Allowed values	[-a-zA-Z0-9]+
Example 1	modus ponens (Q655742) → ax-mp
Example 2	functor (Q864475) → df-func
Example 3	Cayley's theorem (Q179208) → cayley
Example 4	birthday problem (Q339000) → birthday
Source	https://us.metamath.org
Planned use	translate definitions - but not theorems due to size of the catalog - to mix'n'match
Number of IDs in source	45272
Expected completeness	eventually complete (Q21873974)
Implied notability	Wikidata property for an identifier that does not imply notability (Q62589320)
Formatter URL	https://us.metamath.org/mpeuni/$1.html
Wikidata project	WikiProject Mathematics (Q8487137)

Motivation

The metamath set.mm database is a catalogue of formalized definitions and theorems in mathematics. In contrast to other such libraries like the Lean mathlib, it's relatively monolithic, identifiers change very rarely and every identifier has a website attached. This would be a first step into integrating this formalized mathematical knowledge into Wikidata. --Uniwah (talk) 19:02, 21 June 2024 (UTC)[reply]

Discussion

Notified participants of WikiProject Mathematics -- Uniwah (talk) 19:02, 21 June 2024 (UTC)[reply]

Support This would be very useful for the mathematical community! Also the site says "over 23,000 proofs" (and I'm assuming each theorem has at least one proof), against Wikidata's hundreds of millions of items, so we could definitely add all the theorems. (We could also consider them notable, too, since I'm pretty sure the Metamath website is an excellent "serious and publicly available reference" for the purpose of WD:N#2). Duckmather (talk) 19:23, 21 June 2024 (UTC)[reply]

I don't really think all of these can be considered notable - for example, due to the low level nature of the software,

\neg A=B\to A\neq B

and

A\neq B\to \neg A=B

are considered distinct statements Uniwah (talk) 19:30, 21 June 2024 (UTC)[reply]

Well, mathematically speaking that's correct, and at the granularity level Wikidata should be working at, I think that's fine. The Anome (talk) 16:23, 24 June 2024 (UTC)[reply]

Support Very relevant property. --Haansn08 (talk) 04:41, 22 June 2024 (UTC)[reply]

Support An excellent idea. Linking into the formal proof world is an exciting development. 2A00:23C8:728A:2501:B814:9874:2D14:CB6F 09:45, 22 June 2024 (UTC)[reply]

Comment I suggest we do this by first creating new items for every one of these definitions, and then using said to be the same as (P460) to link them to existing items where applicable. The metamath statements in each definition are concise enough that we could use defining formula (P2534) to actually add the metamath symbolic definition for that entity for each item with this property (see https://us.metamath.org/mpeuni/mmdefinitions.html). This could be done easily and automatically at the same time as adding these properties. We can also data-mine the description pages for the English-language names of each definition: for example, df-clim would have the description "limit relation for complex number sequences", and the defining formula " ⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}". I'm happy to do the bot work to make this happen.
Regarding copyright: as far as I'm aware, all of Metamath's database is distrubuted under the CC0 Public Domain Dedication, except for the one file peano.mm, which is LGPL, about which we would need to devote some thought about how it should be handled. (See https://us.metamath.org/copyright.html). However, spot-checking some of the Peano arithmetic definitions on the website itself suggests that it's not based on peano.mm, so this might be a non-problem. The Anome (talk) 16:35, 24 June 2024 (UTC)[reply]
This sounds great! I would be willing (and probably sufficiently knowledgeable) to contribute too, of course, feel free to reach out to me. There's a lot of conventions one would need to sort out though, for example, how should all the syntactic axioms be treated, and how would you turn the metamath terms into proper formulas for P2534?

uses (P2283) could also be utilized to construct the metamath proof graph within wikidata.

More generally speaking, some type for abstract syntact trees (or something similar) would be really helpful for math related content in the long run but that's obviously not realistic at the moment. Uniwah (talk) 19:30, 24 June 2024 (UTC)[reply]
Mercifully Metamath does not use anything more complex than linear strings of symbols, so you don't need to worry about superscripts, subscripts, tables, boxes, or any of the other advanced LaTeX markup; it could all be converted from Unicode symbols to LaTeX entities by fairly simple lookup tables and pattern matching. Also, Metamath has its own ASCII-only low-level representation, which might be another way of achieving the same goal. The Anome (talk) 21:24, 24 June 2024 (UTC)[reply]
Fortunately, someone has already written the necessary code: see https://pylatexenc.readthedocs.io/en/latest/ Which is just as well, because I was not looking forward having to write something like it myself. The Anome (talk) 06:24, 11 July 2024 (UTC)[reply]
See below for an even better solution using Metamath's own software. The Anome (talk) 07:32, 11 July 2024 (UTC)[reply]
@Uniwah, Duckmather, The Anome, Haansn08: Done as Metamath statement ID (P12888). Regards, ZI Jony ^(Talk) 13:01, 10 July 2024 (UTC)[reply]

Notified participants of WikiProject Mathematics OK, strategy time. We have all the source material already available under free licenses, and the Metamath project already have software to perform the Metamath .mm → LaTeX conversion (see section 5.7 of https://us.metamath.org/downloads/metamath.pdf) for the defining equations. Since there are so many of these, I think it would be a mistake to try to auto-match them with existing items about mathematical concepts (at least, unless someone has a viable proposal for doing so) and it would be best to create a new Wikidata items for each Metamath definition, and then the process of either merging the Metamath definition items into existing items or using said to be the same as (P460) can be done by hand. The Anome (talk) 06:30, 11 July 2024 (UTC)[reply]

I'm not super sold on adding every theorem to the database yet - I'd start off just manually merging the definitions, not the theorems, via mix'n'match. But I'm willing to bow to whatever consensus eventually arises Uniwah (talk) 06:41, 11 July 2024 (UTC)[reply]

I was thinking of only adding definitions (whose names all start with df-) to start with. Example: https://us.metamath.org/mpeuni/df-exp.html What is mix'n'match? Is it software? The Anome (talk) 06:44, 11 July 2024 (UTC)[reply]

a tool that allows you to semi-manually match databases against wikidata, see https://meta.wikimedia.org/wiki/Mix%27n%27match/en. It'd reduce the effort going into manual merging and so on, I might prepare a catalog today Uniwah (talk) 06:50, 11 July 2024 (UTC)[reply]

That's fantastic. I hadn't heard of it before. Are you going to post a link to your catalog here when you're done? The Anome (talk) 07:05, 11 July 2024 (UTC)[reply]