The text uses Mizar, a formal language based on Tarsky-Grothendiek set theory for expressing and checking its proofs: http://mizar.org/system/