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