Talk:Metamath

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

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]

'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]

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