# 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.

## Links

- Proofscape
- Holbert Theorem Prover
- Proof Tree Builder - Joomy seems to be working at the SOTA here.
- https://twitter.com/TaliaRinger/status/1373076827879604224?s=19

The Transparent Prolog Machine

## What if you could sonify proofs?

Focused theorem plays some loop based on the tree.