https://boxprover.utr.dk https://boxprover.utr.dk It's an online tool for writing, checking and typesetting Fitch-style proofs in first-order logic, using the

https://boxprover.utr.dk https://boxprover.utr.dk It's an online tool for writing, checking and typesetting Fitch-style proofs in first-order logic, using the Twelf proof assistant under the hood. Its main feature is that it follows the notation from the teaching material 1-1 and offers no assistance in terms of proof tactics in order to help tech the fundamentals of doing formal proofs while still providing feedback when you make mistakes. I built it while TAing a course in logic about 7 years ago, and it is still being used to this day.