Starting with the most recent devel commit MMT includes an export of the Lean prover libraries (via the low-level export files as parsed by the treppline library.