Talk:Metamath

Feedback

That Metamath uses schemes is not a problem according to me. In fact I think when you do math with a paper and a pencil you use schemes without thinking about this. In my opinion using schemes is the normal way to do mathematics for a human being. fl

Is it possible to have a cleaner table of references ? The circumflexe in my opinion is awful.

Surely it is better to distinguish between Metamath and the databases but in that case it would be clearer to speak of set.mm because the Explorer is no more than the html pages generated using set.mm. fl

I think the encyclopedic purpose of Metamath is a very important idea I regret somebody removed it. fl

The paragraph about pedagogy becomes perfectly obscure in my opinion. No school in the world asks its pupils to do symbolic proofs. A simple sight at the proof explorer explains why. I don't understand either the reference to arithmetic ( why arithmetic and not geometry ? ) fl

POV problems

This page has huge POV problems. I am a huge fan of Metamath, but most of this entry probably just needs to be deleted. Also, the picture is a screenshot of a joke theorem (try reading the theorem: it says "April fool"). --Jorend 21:48, 4 October 2006 (UTC)[reply]

What does POV mean ? fl

I really don't like the reference to the April fool's theorem. It is an amuzing theorem but it is also very anecdotical. If its author give the permission I'd like to remove the paragraph dealing this theorem. fl

See WP:NPOV. --Jorend 19:53, 29 November 2006 (UTC)[reply]

I agree that the old page had huge POV problems. I've made a number of changes that I *hope* make it much better. Dwheeler (talk) 21:55, 14 July 2019 (UTC)[reply]

'Truth' in Metamath

Metamath is a proof verification utility - right? But, surely, for there to be confidence in its proof verification capabilities, we much have confidence in whether or not the actual source code of the program is fault tolerant and has been tested to a high standard. Has this been done? Silly idea/thought (completely useless and pointless if one thinks about it), but can metamath be used to prover it's own 'bug-free' nature (ie: it's internal validity)?

These questions are conceivably ill-formed or ill-founded and could do with some cross-examination. --MrASingh

Well in fact the program has not been proved. But that sort of question always remind me a joke: "the mathematician says: strictly speaking it's not possible. The engineer answers: it won't prevent us from going on." So no demonstration of the program. But the algorithm doesn't seem totally silly and the documentation seems to show that the rigor that has been deployed by Norman Megill to realize this program is high. Another remark: the reason why Metamath is not proved is that the program is quite big. But Raph Levien has made a port of Metamath in python. This port is only 600 lines. So it is the sort of program that one can expect to prove so if you have the courage, don't hesitate !

Is it higly tested ? In fact I feel more comfortable to answer that: it is tested everyday for now 10 years. 6000 proofs have been made using Metamath. I don't know if we can consider that as highly tested but it can be called a good test. -- fl 21-Feb-2007

By being mindbogglingly simple, the core of metamath is easy to verify. There are also five independent implementations:[1]

The original, in C,
mmverify.py, in Python,
mmj2, in Java,
Hmm, in Haskell, and
verify, in Lua.

Together, they provide a strong guarantee of the correctness of the proofs.

71.41.210.146 (talk) 01:35, 12 December 2007 (UTC)[reply]

The "truth" of a Metamath theorem may depend upon a) the validity of the Metamath.pdf specification, which documents the base Metamath language and proof verification; b) the correct implementation of the Metamath.pdf specification by programs; c) the validity of the syntax and logic axioms created by users of the Metamath.pdf file format and implementing programs.

Adding complication is Metamath's use of Distinct Variable restrictions controlling substitutions, (see paper by Alfred Tarski, "A Simplified Formalization of Predicate Logic With Identity") instead of the standard free/bound variable substitution scheme. Comprehending this feature of Metamath is a prerequisite for accepting the "truth" of the resulting (meta)theorems. 17-Dec-2007 —Preceding unsigned comment added by 66.81.75.216 (talk) 00:54, 18 December 2007 (UTC)[reply]

Some rewriting needed

I want to expand on, and add to, the criticism above. At the moment, this article is too much like a combination of an advert and a tutorial for Metamath etc. (but Wikipedia is not intended for advertising or for tutorial-oriented works). Also, it does not seem to acknowledge and put Metamath in the context of very much related work (among other formal proof software systems, only Mizar is explicitly mentioned in the lede). What I suggest needs to happen is several things:

1. The point here is not to criticize Mizar which is a very useful and esteemed program but to show Metamath and Mizar are symmetrically opposed regarding their philosophical bases. Mizar wants to have very short proofs (but they also may be as difficult to read as the proofs in a textbook) and Metamath aims at having fully detailed proofs (nothing is hidden but the details may hide the most important steps in the proof). I -- in fact -- regret that somebody rephrases the introduction to let believe that Mizar and Metamath could be concurrent. It was not the spirit of the former introduction. -- fl

Early on in the article, clearly highlight and distinguish between different implementations of the Metamath idea/language. (I don't think all implementations are going to be notable enough to each have their own article, so the "splitting up into separate articles" approach would be a non-starter.) In doing so, try to avoid the "fallacy of conflation", i.e. implying that a problem/advantage is shared by all implementations, if in fact not all implementations have this problem/advantage.

Make it clearer that Metamath is just one of a large range of proof systems available.

Rethink the lede. The lede says that Metamath can be desirable over Mizar because of the level of detail of the proof, but I think this is a false dichotomy. For example, Coq allows you to both create and read proofs at multiple levels of detail, and indeed it's obvious from first principles that this would be possible. So it's not clear to me that the level of detail "enforced" by Metamath is a notable advantage - or even an advantage at all. Sorry to be harsh.
1. Well I persist, Metamath is desirable over Mizar because of its detailed proofs. The reason is that if you want to understand a proof you absolutely need to show everything. Mizar hides a lot of steps (such as a mathematician would do ). It is not a bad thing except that you will never have the opportunity to understand what is not shown. I remember the first time when I understand ( reading a Metamath proof ) that what is called a "reduction to the absurd" in textbooks is no more no less than the application of a specific tautology no more remarkable than a modus ponens in fact. Metamath shows the real nature of that sort of things whereas Mizar hides it. That's what I mean. -- fl
To expand on the previous point: focus less initially on details, and more on advantages and disadvantages compared to other systems. That should be a high priority for any software article where there is any serious competition to the software under discussion - a higher priority than the level of technical details exhibited by this article.
1. To have a page comparing the different systems would be very interesting. But it is certainly a lot of work to get acquainted with only one of those systems... I let you imagine what it means to get acquainted with may of them... And a page of comparisons is not a page about Metamath it's a page about provers. And if you find there are too much details I wonder what you would say if you dive into the docs... :-)

It's a fact that people will evaluate software based on its perceived "amateurishness" or otherwise. Perhaps controversially, I think the page should make it more explicit early on, to what extent (and for which implementations) the project is "amateur", "a research project", or whatever.
1. I hope that all the softwares are as amateurish as Metamath or mmj2 :-). -- fl

—greenrd (talk) 23:22, 12 December 2007 (UTC)[reply]

I rewrote the lede and the language section in an attempt to address many of the criticisms above, since I completely agree. I hope to find time to work on the rest of the article. DanConnolly (talk) 08:12, 28 February 2012 (UTC)[reply]

Italics

I don't understand why you remove the italics to Metamath and to the name of the explorers. It is traditional in books to emphatize the titles of novels, songs, paintings and so on and mutadis mutandis emphatizing should also be used for softwares and internet sites.

Moreover I don't understand why you change the word jansenism for the collocation "low level". Apparently you understood what it meant. -- fl

Metamath is not the title of a book. Further, it goes against the Manual of Style to italicise it throughout the text.

I don't know why the word jansenism was there at all; it doesn't seem appropriate.

CRGreathouse (t | c) 17:49, 4 May 2009 (UTC)[reply]

Excuse me but you don't know anything about Metamath do you ? -- fl

I use the web interface frequently and the downloaded version occasionally. I mostly work with set.mm but occasionally also with peano.mm. I recently corresponded with Norman Megill about a Greasemonkey extension for Metamath I was writing. Does that count as something? You'll have to decide. CRGreathouse (t | c) 18:26, 4 May 2009 (UTC)[reply]

Getting acquainted with it implies to use it to write proofs. You should try. And on the other hand I'll try to ask somewhere perhaps here (Manual of Style) if it is true that it is forbidden to italicise sites and softwares names because I'm a bit puzzled about that strange "law". -- fl

I have no answer concerning softwares names and I more and more wonder if the rule exists. I also notice set.mm is still italicised. I wonder why. Because according to you, italics should be removed -- fl

I didn't say that the italics around set.mm should be removed, but think it should be removed. I haven't decided what the best way would be to have it: plain set.mm, code set.mm, italic set.mm, or something else. Any thoughts? CRGreathouse (t | c) 13:31, 5 May 2009 (UTC)[reply]

You are hard to understand. May I cite yourself: "Further, it goes against the Manual of Style to italicise it throughout the text." Frankly either you italicise Metamath and set.mm (which is the normal way to treat softwares, sites and files names) or you don't italicise any. -- fl

I said "it", not "anything". But it's not that I think set.mm should be italicized, just that I don't know what to do with it. If you were to remove the italics I wouldn't put it back in.

But it's not normal to italicize site names (not on Wikipedia, not elsewhere). In some books filenames are written in monospace, but that's not widespread enough that I'd call it a convention. It's certainly not conventional to italicize filenames.

CRGreathouse (t | c) 15:01, 5 May 2009 (UTC)[reply]

You have also forgotten to unitalicized Mmj2 and Ghilbert'. -- fl

Yes, I missed those. I un-italicized at least one instance of Ghilbert, but I didn't do a global replace like I should have. CRGreathouse (t | c) 19:34, 5 May 2009 (UTC)[reply]

Yes you should. The article was perfectly consistent. All the names of the softwares names were italicised and now half of them are italicised and half of them are not. Definitly I'm very happy you noticed the existence of this page. Remarkable work! -- fl

At the moment my focus is not on writing Metamath proofs but studying the fragments of ZFC it allows (and some it doesn't). I did have Norman add one proof to the database for me recently, but only because I needed it for simplification: axinf. (Note that it hasn't yet propagated to the main server!)

But none of that is relevant to editing the metamath article!

CRGreathouse (t | c) 18:39, 4 May 2009 (UTC)[reply]

Can't hurt either! -- fl

June 2010 edits by Anonymous

Hi, I've reverted the last two June 2010 edits by Anonymous. Metamath is a symbolic proof verifier and is therefore neither required nor expected to have any formal meaning beyond its "symbolism".

The Einstein quote is, in the given context, inappropriate for an encyclopædic article.

Proofs are usually not entered manually into the .mm files but developed and compressed with the metamath proof assistant. BTW, the remark seems out of place.

--GrafZahl (talk) 15:42, 9 August 2010 (UTC)[reply]

"This article needs additional citations for verification."

1 was this added as a joke? software for formal verification needs verification on wikipedia? 2 could the person who added this please insert "verification needed" superscripts at the offending sentence? 3 if no offending sentence is marked would someone bold please remove the "This article needs additional citations for verification." ? — Preceding unsigned comment added by 213.49.120.88 (talk) 01:20, 15 October 2014 (UTC)[reply]

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Metamath. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

Corrected formatting/usage for http://wiki.planetmath.org/cgi-bin/wiki.pl/mmj2

When you have finished reviewing my changes, please set the checked parameter below to true or failed to let others know (documentation at {{Sourcecheck}}).

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—^{cyberbot II}_{Talk to my owner:Online} 22:35, 1 April 2016 (UTC)[reply]

Unexplained cleanup tags

Several years ago, someone added two cleanup tags to this article, alleging that parts of this article were "written like an advertisement." Is there anything we can do to re-write this article in a less WP:promotional tone? Jarble (talk) 22:14, 16 March 2017 (UTC)[reply]

Really I think they're pretty much obsolete now -- the article doesn't read like that now. What do you think? - CRGreathouse (t | c) 09:42, 19 March 2017 (UTC)[reply]

External links modified (January 2018)

Hello fellow Wikipedians,

I have just modified 5 external links on Metamath. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 16:59, 26 January 2018 (UTC)[reply]

Discongruous Reference to Euclid

I think the phrase "The method of proof used by Metamath is far different from what is used in a school context. In schools what is required is the literate, synthetic method of proof developed by mathematicians since Euclid's time.[8][9]" in section Pedagogy is a little discongruous, since in slight contradiction and without matching references

a) Euclid is seen as the father of the axiomatic method, and metamath is axiomatic.

b) The references [8] and [9] don't say something about Euclid, even not the Antique Greeks.

Jan Burse (talk) 23:21, 1 February 2019 (UTC)[reply]

Conflict of Interest (COI) Declarations

If you have any declaration related to Wikipedia's Conflict of Interest (COI) rules, please post them here. Merely using or being interested in Metamath is not a conflict of interest, since Wikipedia articles are more likely to be high quality when the authors know what they're talking about.

David A. Wheeler: I use Metamath, find it interesting, and have contributed to both the program and some databases. However, no one pays me to do Metamath things. I *did* co-author the 2019 edition of the Metamath book, and technically I earn a small royalty from the physical book if people buy it. However, I did not co-author the book to make money, and I don't expect it to make significant money. As evidence, the book continues to be available for download at no charge as a public domain document, and as of 2019-07-12 the royalties have not even covered my expenses (I suspect they never will). I'm declaring here that while I have relevant expertise, I don't believe I have a significant COI. Just as importantly, I'm trying to make my relationship with this article as obvious as possible. Dwheeler (talk) 22:14, 12 July 2019 (UTC)[reply]

Jim Kingdon: although I have contributed to metamath quite a bit (especially iset.mm), I'm not sure that counts as a conflict of interest. Nothing I have done with metamath to date has involved money. Kingdon (talk) 00:57, 15 July 2019 (UTC)[reply]

Plan to remove pedagogy section

Practically the entire "pedagogy" section is speculative. There's a long list of links to other articles, but they don't justify anything. I don't see any experiments that show how well Metamath works in teaching settings, for example. I propose just removing the whole section. — Preceding unsigned comment added by Dwheeler (talk • contribs) 14 July 2019 (UTC)

I agree. I'd be glad to discuss wikipedia policies in more detail (WP:OR springs to mind but there are others), but the short summary is that if the article were going to cover metamath in education, it would a fairly different section from what is here now and there is no particular reason to keep the section as it exists now. I also wonder about using formal proof systems in education as a general topic not as specific to metamath in particular, although that would somewhat depend on the nature of the content and what sources it is based on. So far (especially on the metamath mailing list in the last few days) I've seen a fair bit of discussion of the merits of various ideas about education and metamath, and what metamath is or could be, but little discussion of what belongs in an encyclopedia, which makes me think this is a perfectly plausible topic, but for discussion somewhere other than wikipedia. Kingdon (talk) 23:42, 14 July 2019 (UTC)[reply]

Web browsing claim

The page says: "This project is the first one of its kind that allows for interactive browsing of its formalized theorems database in the form of an ordinary website.[7]"

I doubt "first one" is true. Mizar had a hyperlinked web presentation (JFM) very early (90s?). — Preceding unsigned comment added by 2A06:C701:4727:8400:68E2:B16F:4C56:7644 (talk) 03:37, 11 August 2022 (UTC)[reply]