Naproche-ZF
Naproche-ZF is a new experimental open-source natural theorem prover based on higher-order set theory. Formalizations in Naproche-ZF are written in a controlled natural language embedded into LaTeX and proof gaps are filled in with automated theorem provers. Naproche-ZF aims to scale natural theorem proving beyond chapter-sized formalizations.