Ndpc enables correct, maintainable and formally verified proofs for single sorted predicate logic, whose style follows closely with "hand written" proofs. It can:
- Proof checking
- Generate corresponding Lean4 proofs
- Export to HTML, Latex and Typst
Go to our getting started page for details about installation and basic usage.
An online tutorial is available here. There is also a language reference.
Use github issues or github discussions.
- ndp.vim: (Neo)Vim support for ndp files
- aristotle: GUI frontend for ndpc
- boxproof: Supporting library for Latex backend
- boxproof-typst: Supporting library for Typst backend