Metamath page on Wikipedia

[Norman Megill]

The content of https://en.wikipedia.org/wiki/Metamath is somewhat outdated and doesn't reflect the current focus.  Since I am mentioned several times on the page, I have chosen not to edit it myself because it would feel like a conflict of interest.  But anyone else is welcome to update it.

Suggestions: 
1. The Hilbert Space Explorer and Quantum Logic Explorer shouldn't be mentioned at all.
2. The "explorers" for iset.mm, nf.mm, hol.mm are much more important but aren't mentioned.
3. Using the April Fool joke theorem as an example seems tacky.
4. That Metamath holds a prominent place on Freek's 100 theorem list might be useful to mention.
5. The description of 3rd party verifiers, proof assistants, and IDEs could be updated.

Feel free to add other suggestions here.  Feel free to edit (and hopefully improve) the page at your convenience.

The pages for other provers such as Mizar, HOL Light, Coq, Isabelle, etc. might offer ideas.  However, they are sometimes shorter than Metamath's, and there doesn't seem to be consistency in the length, style, or level of detail.  So in the end you have to use your own judgment.

Thanks,
Norm

[Jim Kingdon]

Good point about the conflict of interest (there is lots more detail at https://en.wikipedia.org/wiki/Wikipedia:Plain_and_simple_conflict_of_interest_guide - one interesting suggestion of which is that posting to the Talk page of the article is a lot more kosher than editing the article itself - in a case like this where the article is about yourself or your organization).

The screen shot, in addition to picking a better theorem than the april fool's one ("tacky" might be fair, but "not very illustrative of what is really in set.m" is sort of maybe the way I'd say it), should look better (which is probably just be a matter of screenshotting a mpeuni rather than mpegif page).

There is a fair bit of just general updating which would be nice, that's probably the #1 thing which stands out. I did just fix one out-of-date statement about what set.mm covers, but there's more of this sort of thing.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3c546632-f6a2-434c-a3d5-29a2baba8e71%40googlegroups.com.

[Thomas Brendan Leahy]

To be honest, I feel it quite inappropriate to post this page, inasmuch as anyone reading this post probably - bar an errant search - shouldn't be editing that page.

[Mario Carneiro]

The problem with small communities is that *everyone* has a conflict of interest to some degree. Either you know nothing about the topic and shouldn't be writing about it, or you know or at least recognize a significant number of people involved and COI results. I know all the reviewers for my papers, and vice versa. The best you can hope for is to try to be objective and don't be too picky about claiming COI from the more tenuous connections, because otherwise you won't get anything done.

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/52825472-f500-4a9f-a3d2-a04de4432e99%40googlegroups.com.

[Jon P]

It looks like they have a system for disclosing conflicts of interest. That might help people feel more comfortable with editing.

Another option would be to try and contact a mathematics or computer science editor and to ask them to rewrite the page. Not sure how easy that is though.

[Benoit]

I cleaned up the introduction and the "Databases" section. In particular:
* Mentioned the 3rd place in the "100 theorems" challenge.
* Restructured the "Databases" section to better reflect the relative importance of the databases, adding intuitionistic, NF, HOL, and putting the older databases in a separate subsection.
* Removed excessive details: writing that set.mm implements square roots and exponentiation and whatnot is really too much detail for such a wikipedia page.

What remains to be done:
* There are many broken links among the references...
* "Pedagogy" section: I would simply remove the whole thing: it merely expresses someone's opinions (which, FWIW, I happen to disagree with).  It looks like it was written by FL? I you read me, Frédéric, what's your opinion? Can we delete it? Remember that some of the harshest criticisms made to Bourbaki were actually directed to people wanting to use ideas from their Eléments as pedagogical tools.
* April's fool screenshot: replace with a screenshot of mpeuni/id1.html ? Can someone do it?
* Section "The Metamath language": I would remove most of the "how to" part, since it is in the Metamath book, where it belongs, and wikipedia is not a "how to" nor a substitute to the Metamath website or book.
* Other sections

Benoit

[Jim Kingdon]

Those edits look good; thanks. I like the way that you described the scope not to the detail of things like square root, but do include general topics like set theory, complex analysis, topology, etc.

As for Pedagogy, I'd be fine with removing this section. I could see something (moderately different from what is there now) about using metamath in education (I think maybe I saw a few papers in Google scholar on that), although I'm not sure that's enough of a thing that it necessarily needs a mention.

On July 12, 2019 6:41:47 AM PDT, Benoit <benoit...@gmail.com> wrote:

I cleaned up the introduction and the "Databases" section. In particular:
* Mentioned the 3rd place in the "100 theorems" challenge

* Restructured the "Databases" section to better reflect the relative importance of the databases, adding intuitionistic, NF, HOL, and putting the older databases in a separate subsection.
* Removed excessive details: writing that set.mm implements square roots and exponentiation and whatnot is really too much detail for such a wikipedia page.

What remains to be done:
* There are many broken links among the references...

* "Pedagogy" section: I would simply remove the whole thing: it merely expresses someone's opinions (which, FWIW, I happen to disagree with).  It looks like it was written by FL? I you read me, Frédéric, what's your opinion? Can we delete it? Remember that some of the harshest criticisms made to Bourbaki were actually directed to people wanting to use ideas from their Eléments as pedagogicals tools.
* April's fool screenshot: replace with a screenshot of mpeuni/id.html ? Can someone do it?

[fl]

* "Pedagogy" section: I would simply remove the whole thing: it merely expresses someone's opinions (which, FWIW, I happen to disagree with).  It looks like it was written by FL? I you read me, Frédéric, what's your opinion? Can we delete it? Remember that some of the harshest criticisms made to Bourbaki were actually directed to people wanting to use ideas from their Eléments as pedagogical tools.

1) I'm a little confused. I see no mention of Bourbaki's treatise on this page. I'm talking about a proof checker from Juha Arpiainen called Bourbaki. It's not the same thing.

2) On the other hand, if someone wants to read Bourbaki's treatise, one of the best things to do is to implement the proofs in set.mm. That I'm sure of it. And it is one of the most beautiful presentations (the most beautiful) of the concept of structure.  And again I'm 

in favour of textual references in set.mm. If there is none, no one will read the material.


3) Rereading what I wrote many years ago about the possible use of metamath in high school or college (the pedagogy section), 

I still agree with this view. Change the title of the section ! " Is metamath suitable for use in high school and college?")

4) Leave some substance to the article anyway. It should be a guide to where and when to use metamath and where and when not to use it.

-- 

FL

[fl]

I will give my opinion on what should be in the wikipedia article. Mainly two issues: a) the operating principles of metamath. b) In which cases it can be used and in which cases it cannot be used.

From that point on, it seems to me that this is the right blueprint:

1) operating principles. The substitution algorithm used by metamath. The peculiar provisos of metamath.

2) Comparison with other provers. Logic plugged into the software vs simple verification of substitutions. Provers using a typed lambda calculus vs provers using FOL + ZFC. Possibility to use any logic in metamath. Only restriction: it's not suitable for Gentzen style. 

3) Tools: mainly mmj2 in O'cat version. Carneiro's is not yet ready. Except for the algorithm checking that the system is sound. Using metamath itself to enter a proof is not recommended: there is no good syntactic interpreter. Use only this tool to generate html pages or to check your database is correct.

4) Databases. Anything you want by indicating the limits of use of each. The database on the New Foundation. It is correctly commented and there are textual references. The intuitionism database seems to have some interesting comments on the entry page and on the axioms but then it's much more 

succinct.

5) When to use metamath? For all kinds of logics: classical, intuitionist, modal, lambda calculus typed or not.

For set theory. 

Metamath is relatively well adapted for structures (algebraic, topological) and for everything that resembles structures: geometry (Euclid's or Tarski's), graph theory, category theory.

On the other hand, metamath is completely unsuitable for concrete calculations. If you have to do multiplication, choose another checker.

Metalogics is not so good either. And algorithmic studies must be a little cumbersome. But it remains to be confirmed.

6) Do not use metamath under the baccalaureate.

Voilà: it seems to me that this should make a correct page.

-- 

FL

[vvs]

On Saturday, July 13, 2019 at 1:56:22 PM UTC+3, fl wrote:

On the other hand, metamath is completely unsuitable for concrete calculations. If you have to do multiplication, choose another checker.

Sure, but at least it's compatible. I can imagine MM0/1 could implement CAS on top of it, when and if it's ready of course.

[Benoit]

Thanks Jim and Frédéric.

Frédéric: I saw that you did not mention Bourbaki's treatise on the wikipedia page.  My point was simply that the use of Bourbaki's ideas as pedagogical tools (which was not advocated by members of the Bourbaki group) was strongly (and in my opinion, rightly) criticized (a few classes in the 1970's suffered the "mathématiques modernes", having to draw potatoids and bijections in middle school, but fortunately this craze only lasted a few years).  I think that similarly, the use of Metamath as a pedagogical tool should be taken with care (to me, it could be used as secondary material in introduction to logic classes, but not much else).

If Frédéric and Jim can word a more balanced view, I encourage you to edit the wikipedia page section.

I agree with Frédéric that the Bourbaki treatise is a wonderful book, and it really emphasizes the unity of mathematic (no 's'!).  I've read big chunks of the first five books and "Lie groups and algebras" and spectral theory.  It is a reference book, not a textbook or a pedagogical device.

Benoit

[vvs]

On Sunday, July 14, 2019 at 6:08:28 PM UTC+3, Benoit wrote:

I think that similarly, the use of Metamath as a pedagogical tool should be taken with care (to me, it could be used as secondary material in introduction to logic classes, but not much else).

I disagree. For me the usual treatise of logic is mostly artificial and this is probably the only universally available tool to make it more concrete. There are attempts to interpret theoretical results in application to digital circuits or programming, but that's not nearly enough. Actually, I'm reading introductory texts and solving examples first and seeking for more deep explanations only after. In fact only this way I was able to really understand some definitions and theorems in textbooks. I think that's why such things as incredible.pm or Jape were invented in the first place.

But I agree that it's not for people who has not yet built any semantic model at all, e.g. kids in school.

[fl]

For me the usual treatise of logic is mostly artificial and this is probably the only universally available tool to make it more concrete.

I don't fundamentally disagree with that. Simply I think that if you want to teach logic with software you have to use natural deduction with a system where the context stack is very apparent at each step and where the problem of provisos is simplified as much as possible. I feel that there are systems where when you delete a quantifier, the variable is replaced by a constant. It seems to me to be the clearest system for a beginner.

And then the teacher must analyze on the blackboard a textual proof to clearly show the relationship between textual proof and formal proof and that juggling between the two forms is acquired.

Finally, I find that a system where the human-machine interface is very visual is better.

In short, that's why I think Metamath is not the best educational tool.

-- 

FL

[fl]

> Finally, I find that a system where the human-machine interface is very visual is better.

And there must also be a preliminary sequence where the most frequent reasonings and reasoning errors are explained on textual examples to keep all this meaningful.

-- 

FL

[fl]

 I feel that there are systems where when you delete a quantifier, the variable is replaced by a constant. It seems to me to be the clearest system for a beginner.

In some presentations, they call it a "witness" I think.

 

-- 

FL

[fl]

I agree with Frédéric that the Bourbaki treatise is a wonderful book, and it really emphasizes the unity of mathematic (no 's'!).  I've read big chunks of the first five books and "Lie groups and algebras" and spectral theory.  It is a reference book, not a textbook or a pedagogical device.

 Yes, but at the stage where set.mm is at, we can use it without any problem: it's at the same level.

 

-- 

FL

[vvs]

On Sunday, July 14, 2019 at 10:30:04 PM UTC+3, fl wrote:

Finally, I find that a system where the human-machine interface is very visual is better.

In short, that's why I think Metamath is not the best educational tool. 

But this isn't Metamth's fault in particular but merely mmj2's.

And there must also be a preliminary sequence where the most frequent reasonings and reasoning errors are explained on textual examples to keep all this meaningful.

Right, that's where introductory texts should have their way. And any software assistant should have a feedback, i.e. red lines or shaded inaccessible rules. Present Metamath tools lack that, but it's irrelevant to language.

[fl]

But this isn't Metamth's fault in particular but merely mmj2's.

Mmj2 was designed as an editor to enter the proofs not as a pedagogical tool. Don't blame it. It does its job perfectly.

 

-- 

FL

[fl]

Finally, I find that a system where the human-machine interface is very visual is better.

At the same time, I think we should keep the simple metamath substitution algorithm because a beginner will understand that.  The other systems are much more complicated and difficult to understand.

Something like nat.mm would finally be fine if we could make a provisios system simpler than the $d statements.

 

-- 

FL

[vvs]

On Sunday, July 14, 2019 at 10:58:41 PM UTC+3, fl wrote:

Mmj2 was designed as an editor to enter the proofs not as a pedagogical tool. Don't blame it. It does its job perfectly.

It might be a good editor but not so a good assistant. Good software should respect a separation of concerns, i.e. language should not leak to interface design and rendering of its results. Jape has been pretty good pedagogical tool because of that and nothing prevents Metamath from beating it.

Mmj2 has a macro system implemented in Javascript, but I think it's pretty limited and never saw a tutorial for it. My hopes now lie with MM0/1 which should take these mistakes into account.

[David A. Wheeler]

On Sun, 14 Jul 2019 12:30:04 -0700 (PDT), "'fl' via Metamath" <meta...@googlegroups.com> wrote:
> I don't fundamentally disagree with that. Simply I think that if you want
> to teach logic with software you have to use natural deduction with a

> system...

> In short, that's why I think Metamath is not the best educational tool.

I'm not sure that these claims belong on the Wikipedia page
about Metamath, though. If there's a scientific study that proves these
claims, then cite it! Otherwise, they're simply reasonable opinions.

I think we have something of a counter-example: I believe at least one
high school student learned logic via Metamath/set.mm,
and contributed a number of proofs.

I'm beginning to think the whole "Pedagogy" section should just be removed from
the Wikipedia page. It's mainly opinion unsupported by any rigorous study.

--- David A. Wheeler

[fl]

Hi David, 

As you wrote a book with Norm on Metamath and there are copyright issues, I wonder if you should not refrain from interfering 

in the process of writing the wikipedia page.  It could be considered a conflict of interest.

-- 

FL

[fl]

 

It might be a good editor but not so a good assistant.

We agree.

 

Good software should respect a separation of concerns, i.e. language should not leak to interface design and rendering of its results. Jape has been pretty good pedagogical tool because of that and nothing prevents Metamath from beating it.

Speaking of interfaces, this one looks good to me. 

https://proofs.openlogicproject.org/

Anyway if someone created an assistant he should keep the metamath substitution algorithm very apparent. Because that's very strong.

-- 

FL

[David A. Wheeler]

I was also concerned about that, so I read the conflict of interest page. I think I'm okay. I posted a justification on the talk page (which ensures that my relationship is not a secret). If people had to recuse themselves from all things they knew, Wikipedia would be worse off.


--- David A.Wheeler

[fl]

I was also concerned about that, so I read the conflict of interest page. I think I'm okay. I posted a justification on the talk page (which ensures that my relationship is not a secret). If people had to recuse themselves from all things they knew, Wikipedia would be worse off.

These are the usual arguments of people with conflicts of interest: They are competent; they are as honest as Job; nothing was secret.

As if the others were not competent!

There are copyright issues. That's all. It might put Norm in a position to explain himself later. It can be unpleasant. 

-- 

FL

[fl]

If there's a scientific study that proves these claims, then cite it! Otherwise, they're simply reasonable opinions.

 

Is it evidence-based? Of course not, it is no evidence-based. I'm not the Food and Drug Administration or NASA. "Evidence-based" has become the argument for killing any conversation in one shot.

Let's get back to reality. Let us return to humanism. Correct reasonings on probable truths will suffice.  It did the job for 2500 years, it can still do it. This was Leibniz' and Galileo's way of thinking, no less.

And when we see what food, ecological and climatic disasters the "scientific" organization of society has led us to, we may have doubts about "evidence-based" things. There is obviously something wrong somewhere.

Coca-Cola and Monsanto, the evidence-based things they know how to manage them. Through conflicts of interest, incidentally.

-- 

FL

[vvs]

On Monday, July 15, 2019 at 3:30:20 PM UTC+3, fl wrote:

If there's a scientific study that proves these claims, then cite it! Otherwise, they're simply reasonable opinions.

 

Is it evidence-based? Of course not, it is no evidence-based. I'm not the Food and Drug Administration or NASA. "Evidence-based" has become the argument for killing any conversation in one shot.

Sorry for interfering. I think that statement was a bit provocative: science can not *prove* (in logical sense) anything by evidence if it isn't invented, but can only disprove *universal* claims by counter-example. OTOH Wikipedia has a policy which forbids original research, so references to secondary sources are required. I was bitten by this rule several times.

But let us not turn personal, please. And there is no reason to appeal to geopolitics or universal evil (whatever that could be that instant), not the least because it's off-topic here and would fall on deaf ears. This is just my humble opinion, of course.

[fl]

But let us not turn personal, please.

OK, let's come back to our point: what should be the topics covered by the wikipedia article and with what outline.

-- 

FL

[fl]

2) Comparison with other provers. Logic plugged into the software vs simple verification of substitutions. Provers using a typed lambda calculus vs provers using FOL + ZFC. Possibility to use any logic in metamath. Only restriction: it's not suitable for Gentzen style. 

 

So is it possible to add a paragraph that compares the main principles used by Metamath with those used by other checkers? 

Can we put it after the paragraph dedicated to the Metamath principles.

-- 

FL

[fl]

I think we have something of a counter-example: I believe at least one
high school student learned logic via Metamath/set.mm,
and contributed a number of proofs.

I think I remember who you're talking about. A teenager who no longer understood anything about math and who had managed to put the pieces of the jigsaw together by exploring set.mm in his spare time in his room. And he ended up taking math classes again at the university.

Just quote his opinion in the "Pedagogy" section after mine, the way a good journalist in a good newspaper like the New York Times would quote divergent opinions or experiences on a given subject. And this without having to go into scientistic delusions like "evidence-based".

I would just point out that he and I are not talking about the same situation: he is talking about hundreds of hours he spent on his own on set.mm, and I am talking about a group course to less motivated students. I challenge any teacher to motivate his students by taking as a starting point the hundreds of theorems of propositional logic in set.mm.

--
FL

[fl]

Just quote his opinion in the "Pedagogy" section after mine, the way a good journalist in a good newspaper like the New York Times would quote divergent opinions or experiences on a given subject. And this without having to go into scientistic delusions like "evidence-based".

 

I'm sorry, I forgot: you have a conflict of interest. I don't know how to do it then.
 
--
FL

[vvs]

On Tuesday, July 16, 2019 at 7:57:31 PM UTC+3, fl wrote:

Just quote his opinion in the "Pedagogy" section after mine, the way a good journalist in a good newspaper like the New York Times would quote divergent opinions or experiences on a given subject. And this without having to go into scientistic delusions like "evidence-based".

Actually, Wikipedia wants secondary sources and not just someone's opinion. That's why I stopped contributing to it a long time ago. There are hordes of moderators which don't know a thing about subject but are trigger happy to remove anything suspicious. I just don't have so much time and motivation. But some professional researcher might have it all.

I would just point out that he and I are not talking about the same situation: he is talking about hundreds of hours he spent on his own on set.mm, and I am talking about a group course to less motivated students. I challenge any teacher to motivate his students by taking as a starting point the hundreds of theorems of propositional logic in set.mm.

That guy who invented incredible.pm has a paper about such experiences. And he said something about 14 academic hours if I'm not mistaken. This counts as a scientific evidence, but not logical proof of course. Though, Wikipedia should be happy by this reference.

[fl]

Actually, Wikipedia wants secondary sources and not just someone's opinion.

Yes, they are unbearable. They don't read a single book, they ask you for quotations and references to the word all over the place. It is their weapon of mass destruction after evidence-based. You say that the proofs in Metamath are a little too detailed for beginners, they ask you for a quote. Why a quote? It's a personal judgment. How a quote, in other words someone else's personal judgment, would be more appropriate than mine. And he gives you as a counter-example the proofs of Euclid which would also be detailed. Is Euclid formal mathematics? Did Euclid do his proofs by exhibiting the details of variable replacements? Did he take the provisos expressly into account  ? They conceive any article as a commercial promotion. You can say that the thing is good, really very good, really very very good if you had the audacity to express the slightest reservation on a very limited point, they have their heads turned upside down.

There is no way to ask them to give references to a mathematics book for completely standardized theorems and definitions, in order to have a textual companion to formulas that are sometimes a little too formal and given without explanation, but then for a particular software for which your experience is no less valid than that of another, you are asked to quote an entire library.

-- 

FL

[fl]

Yes, they are unbearable. They don't read a single book, they ask you for quotations and references to the word all over the place.

This is all a parody of objectivity.

-- 

FL

[vvs]

On Wednesday, July 17, 2019 at 12:26:40 PM UTC+3, fl wrote:

Why a quote? It's a personal judgment. How a quote, in other words someone else's personal judgment, would be more appropriate than mine.

That way you can prove that you are a member of a cabal. Really, references to the past won't hold anymore because these are quite different times. Why? Because it works for many and you are part of a bigger society. Wikipedia plays by the rules, so we have little choice.