Link Search Menu Expand Document

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.

The Transparent Prolog Machine

What if you could sonify proofs?

Focused theorem plays some loop based on the tree.