Well, there is the Naproche-SAD project: https://github.com/Naproche/Naproche-SAD/blob/master/README.md https://github.com/Naproche/Naproche-SAD/blob/master/RE

Well, there is the Naproche-SAD project: https://github.com/Naproche/Naproche-SAD/blob/master/README.md https://github.com/Naproche/Naproche-SAD/blob/master/README.... > Proof Checking of Natural Mathematical Documents, with optional support for Isabelle Prover IDE. The goal is to be able to proofcheck from Latex directly. Most of the machinery is (used to be) written in Haskell. It is definitely a cool project, and they could definitely use help.