Daniyal Akif, a math undergrad student at UT Austin, has updated Kevin Klement’s old Fitch proof editor and checker. If you’re learning or teaching natural deduction from forall x: Calgary, it may be useful to you. New features include:
- Support for proofs in modal logic.
- A “hint” feature that suggests the next formula or justification you should try.
- An “export” feature that will save your proof either in plain text or as a fitch.sty
fitchproofenvironment.
You can use the proof editor at ndprover.org. The source code is on Github, where you can also provide feedback and report bugs.