Re: [mizar] "Formalized Mathematics"

[Jesse Alama <alama@stanford.edu>]

Roman Matuszewski <romat@mizar.org> writes:

> Additionaly, please observe that 5 articles published
> in "Formalized Mathematics" are in the first 20 most
> cited computer science articles in the CiteSeerX:
> http://citeseerx.ist.psu.edu/stats/articles;jsessionid=D28942507FE29084C3D690F0B650872A

These five articles ("Tarski-Grothendieck set theory", "Properties of
subsets", "Functions and their basic properties", "Relations and their
basic properties", "Functions from a set to a set") are in the top 20
for a simple reason: the articles in the citeseer database that cite
them are also FM articles, and virtually all the MML depends on TARSKI.

The citation structure of FM articles is rather different from that of
other journals.  In mizar everything -- everything! -- that is logically
required for your article gets cited.  If other journals required
citations like that, then the citeseer top 20 would probably look very
different.  (What might be at the top of the pile?  Feller's probability
books?  Spivak's Calculus?  Halmos's Naive Set Theory?)

Jesse

-- 
Jesse Alama (alama@stanford.edu)