  We argue that the language of Zermelo Fraenkel set theory with definitions
and partial functions provides the most promising bedrock semantics for
communicating and sharing mathematical knowledge. We then describe a syntactic
sugaring of that language that provides a way of writing remarkably readable
assertions without straying far from the set-theoretic semantics. We illustrate
with some examples of formalized textbook definitions from elementary set
theory and point-set topology. We also present statistics concerning the
complexity of these definitions, under various complexity measures.
