Wikidata:Property proposal/Metamath statement label

‎Metamath statement label

Return to Wikidata:Property proposal/Authority control

Under discussion

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)Metamath statement labelax-mp
Example 2	functor (Q864475)Metamath statement labeldf-func
Example 3	Cayley's theorem (Q179208)Metamath statement labelcayley
Example 4	birthday problem (Q339000)Metamath statement labelbirthday
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]