  As one of the longest-running computer-assisted formal mathematics projects,
large tracts of mathematical knowledge have been formalized with the help of
the Mizar system. Because Mizar is based on first-order classical logic and set
theory, and because of its emphasis on pure mathematics, the Mizar library
offers a cornucopia for the researcher interested in foundations of
mathematics. With Mizar, one can adopt an experimental approach and take on
problems in foundations, at least those which are amenable to such
experimentation. Addressing a question posed by H. Friedman, we use Mizar to
take on the question of surveying the sentence complexity (measured by
quantifier alternation) of mathematical theorems. We find, as Friedman
suggests, that the sentence complexity of most Mizar theorems is universal
($\Pi_{1}$, or $\forall$), and as one goes higher in the sentence complexity
hierarchy the number of Mizar theorems having these complexities decreases
rapidly. The results support the intuitive idea that mathematical statements,
even when carried out an abstract set-theoretical style, are usually quite low
in the sentence complexity hierarchy (not more complex than
$\forall\exists\forall$ or $\exists\forall$).
