Why are proof assistants so unfriendly?
Inspired by Katherine Ye's Proof assistants as a tool for thought.
Some logic can be a game: see The Incredible Proof Machine:
Goal-directed games obviously aren't always great though.
- Holbert Theorem Prover
- Proof Tree Builder - Joomy seems to be working at the SOTA here.
What if you could sonify proofs?
Focused theorem plays some loop based on the tree.