Abstract 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 "Image missing" 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}$$ 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.

Abstract "Image missing" is an emerging natural proof assistant that accepts input in the controlled natural language ForTheL. "Image missing" is included in the current version of the Isabelle/PIDE which allows comfortable editing and asynchronous proof-checking of ForTheL texts. The dialect of ForTheL can be typeset by "Image missing" into documents that approximate the language and appearance of ordinary mathematical texts.

Naproche is an emerging natural proof assistant that accepts input in a controlled natural language for mathematics, which we have integrated with LaTeX for ease of learning and to quickly produce high-quality typeset documents. We present a self-contained formalization of the Mutilated Checkerboard Problem in Naproche, following a proof sketch by John McCarthy. The formalization is embedded in detailed literate style comments. We also briefly describe the Naproche approach.