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.
Counter: proof assistants are about clear thinking. Many prefer paper and pencil still.
- 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.
So, how can a proof assistant aid thought, not just proof tree walking?