Description of the MPTP system translating the Mizar Mathematical Library for first-order automated theorem provers.
