[mizar] A quote

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

In: 
	math.HO/0311260 [<http://xxx.lanl.gov/abs/math.HO/0311260>abs,
	+<http://xxx.lanl.gov/ps/math.HO/0311260>ps,
	+<http://xxx.lanl.gov/pdf/math.HO/0311260>pdf,
	+<http://xxx.lanl.gov/format/math.HO/0311260>other] :

	Title: Computer theorem proving in math
	Authors: <http://xxx.lanl.gov/find/math/1/au:+Simpson_C/0/1/0/all/0/1>Carlos T. Simpson
	Subj-class: History and Overview; Category Theory; Algebraic Geometry; Differential Geometry; Logic

p. 6 we read:

  The first major project involving a large number of people was Mizar;
  it is still ongoing, and led to the Journal of Formalized Mathematics
  which has been publishing articles verified in the MIZAR system since
  at least 1989. The mathematical orientation of most of the articles is
  a little bit far from the mainstream of what we call standard
  mathematics.

One may not agree with the above (especially in the light of the rest of the
paper).  However, it is inevitable that people will be discouraged by the
amount of garbage in MML.  In this light the "weak types" can wait.


-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr