The Naproche-ZF Theorem Prover (Short Paper)

Naproche-ZF is a new experimental open-source natural theorem prover based on set theory; formalizations in Naproche-ZF are written in a controlled natural language embedded into and proof gaps are filled in with automated theorem provers. Naproche-ZF aims to scale natural theorem proving beyond chapter-sized formalizations. In contrast to the \(\mathbb {N}\) aproche system, the new system uses an extensible grammar-based approach, has more efficient proof automation, and enables larger interconnected formalizations based on a standard library.