Talk:Metamath
From Wikipedia, the free encyclopedia
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)
- 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
[edit] '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
