On Mon, 28 Jul 2008, Jesse Alama wrote:
Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:at http://octopi.mizar.org/~urban/dupl.html is a list of more than 1000 MML duplications.How many of these are caused by the fact that, in some articles, some authors prove results without "exporting" them using the theorem keyword?
I guess more than half. There are funny situation when the lemma is proved more than once (even in one file :-), and when it is equivalent to more than one theorem :-). A more "legal" source of duplications is when a cluster is justified by a lemma or a theorem.
It is frustrating to find out, after looking for a theorem in the MML, that it is off-limits to you because the author thought that a result should be just a lemma rather than a theorem. (Down with lemmas, I say! Make every proved result available to everyone, not just yourself.)
I agree, "Mizar theorems" are no match for what mathematicians grade as "theorems" anyway. Unless a lemma is only needed to prove a clearly (from a Mizar point of view) stronger result, it should be exported as a "Mizar theorem".
Lemmas can even lead to odd situations such as Lm1 in ZFMISC_1 and ZFMISC_1:37.
There are quite a few situations like that, my conjecture is that this is done to keep the theorem numeration stable.
Josef