<h1 id="why-are-proof-assistants-so-unfriendly">Why are proof assistants so unfriendly?<a aria-hidden="true" class="anchor-heading icon-link" href="#why-are-proof-assistants-so-unfriendly"></a></h1>
<p>Inspired by Katherine Ye's <a href="https://www.cs.cmu.edu/~kqy/resources/coq_tools_for_thought.pdf">Proof assistants as a tool for thought</a>.</p>
<p>Some logic can be a game: see <a href="https://incredible.pm/">The Incredible Proof Machine</a>:
<img src="/inquiry/assets/images/2021-01-29-01-40-51.png"></p>
<p><a href="https://www.youtube.com/watch?v=w1_zmx-wU0U">Goal-directed games</a> obviously aren't always great though.</p>
<p>Counter: proof assistants are about clear thinking. Many prefer paper and pencil still.</p>
<h2 id="links">Links<a aria-hidden="true" class="anchor-heading icon-link" href="#links"></a></h2>
<ul>
<li><a href="https://royalroadmath.org/newpfsc.html">Proofscape</a></li>
<li><a href="http://liamoc.net/holbert/">Holbert Theorem Prover</a></li>
<li><a href="https://joom.github.io/proof-tree-builder/src/">Proof Tree Builder</a> - <a href="https://www.cs.princeton.edu/~ckorkut/">Joomy</a> seems to be working at the SOTA here.</li>
<li><a href="https://twitter.com/TaliaRinger/status/1373076827879604224?s=19">https://twitter.com/TaliaRinger/status/1373076827879604224?s=19</a></li>
</ul>
<p><img src="/inquiry/assets/images/2021-02-01-17-49-32.png"></p>
<p><a href="https://core.ac.uk/download/pdf/81925898.pdf">The Transparent Prolog Machine</a></p>
<p><a href="https://twitter.com/kamatsu8/status/1449178161665777666?s=21">https://twitter.com/kamatsu8/status/1449178161665777666?s=21</a></p>
<p><a href="https://twitter.com/totbwf/status/1450605827119673344?s=21">https://twitter.com/totbwf/status/1450605827119673344?s=21</a></p>
<h2 id="what-if-you-could-sonify-proofs">What if you could sonify proofs?<a aria-hidden="true" class="anchor-heading icon-link" href="#what-if-you-could-sonify-proofs"></a></h2>
<p>Focused theorem plays some loop based on the tree.</p>
<h2 id="counter-thread">Counter thread<a aria-hidden="true" class="anchor-heading icon-link" href="#counter-thread"></a></h2>
<p><a href="https://twitter.com/cattheory/status/1470762265288785921?s=21">https://twitter.com/cattheory/status/1470762265288785921?s=21</a></p>
<p><a href="https://twitter.com/sarah_zrf/status/1470788248695881733?s=21">https://twitter.com/sarah_zrf/status/1470788248695881733?s=21</a></p>
<p>So, how can a proof assistant aid thought, not just proof tree walking?</p>
<p><a href="https://www.irit.fr/~Martin.Strecker/Publications/ticttl_panda2011.pdf">https://www.irit.fr/~Martin.Strecker/Publications/ticttl_panda2011.pdf</a></p>
<p><a href="https://mobile.twitter.com/disconcision/status/1491571996718628866">https://mobile.twitter.com/disconcision/status/1491571996718628866</a></p>
<hr>
<strong>Backlinks</strong>
<ul>
<li><a href="/inquiry/notes/FEssYKYzijiy1lvq3n2vh">Organic Chemistry if it was Fun</a></li>
<li><a href="/inquiry/notes/77343d6f-26f6-4e9f-8caf-e592c0548a31">Domain-Learning with Computational Microworlds</a></li>
</ul>

Why are proof assistants so unfriendly?


This is [Max Krieger](https://a9.io)'s "inquiry" page. I guess it's like a [Digital Garden](https://github.com/MaggieAppleton/digital-gardeners). But I'm not trying to upload my Second Brain to it. Just want to share some half-baked ideas. One source of inspiration for this was Kevin Lynagh's ["Collaboration ideas"](https://kevinlynagh.com/ideas/). See also Sharif Shameem's ["Questions"](https://sharif.io/questions/).

It was made with [Dendron](https://dendron.so).

Take everything I write here (well, everywhere) with a grain of salt. That said I'm always happy to talk about anything on here.

The pages definitely don't adhere to [Andy's Evergreen Notes](https://notes.andymatuschak.org/z4SDCZQeRo4xFEQ8H4qrSqd68ucpgE6LU155C) pattern, I hope one day they do.

Feel free to add [a PR or issue to the repo](https://github.com/maxkrieger/inquiry) to discuss any of these in public!

## Guide

Here are some of my favorite/extensive pages:

- [[Linear algebra as spreadsheet|projects.linear-algebra-spreadsheet]]
- [[Domain learning for computational microworlds|rethinking-media.microworld-languages]]
- [[Linux DE prototyping|projects.linux-desktop]]
- [[System Archaeology|projects.system-archaeology]]

---

![](/assets/images/2021-03-18-20-55-10.png)

[El Lissitzky, The Constructor (self-portrait, 1924)](https://commons.wikimedia.org/wiki/File:El_Lissitzky_The_Constructor,_self-portrait,_gelatin_silver_print,_107%C3%97118_mm,_1924_London,_Victoria_and_Albert_Museum,_Inv._PH142-1985.jpg)
