70 karma · joined December 23, 2025
[1] https://www.cs.cornell.edu/courses/cs3110/2025sp/
[2] https://pragprog.com/titles/tpp20/the-pragmatic-programmer-2...
I’ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2].
For me, Pirsig put it best: "Quality is the goal of Art." I too struggled to understand Pirsig's full metaphysical hierarchy of Quality, but this quote gets at the core of the similarities I saw in these books.
Pirsig was concerned with teaching his students writing and maintaining his motorcycle. Berry was concerned with doing fulfilling and meaningful work on the farm. The MIT hackers were concerned with finding The Right Thing: "the unique, correct, elegant [program]." All of these individuals were concerned with some notion of Quality.
Interestingly, they all viewed what they were doing as a form of art. A colleague remarked, "Sounds like art," to Pirsig upon hearing his ideas on Quality, to which he responded, "Well, it is art." Levy identifies "You can create art and beauty on the computer." as one of the tenets of The Hacker Ethic. "[A]ll serious computer programs are expressions of an individual." This was the first clue to me that they were all talking about the same thing.
Like art, Quality is more a description of a process than product. And the Quality way of working that all three books discuss is very much the same. For me, it is exactly the defining characteristics of the artistic process. Through their work, an artist expresses themselves. They make contact with their medium, be that motorcycle, field, code, or painting. They make choices. Their medium responds. Both evolve with each other. The process is inherently experimental. Importantly, their medium imposes limitations and constraints.
I gave this talk back in 2024, two years after I took the course. At the time, I was frustrated with my lack of artistic output post-graduation. These readings made me realize my creative/artistic outlet had just changed for the time being. I took a lot of solace in that. Recently, I've been trying to understand how AI fits into my picture of Quality programming.
If you've come this far, you might be interested to see some of my image & algorithm work [1]. The decluttering, exaptation exhibition was the culmination of the class and an independent study.
I should also mention Shop Class as Soulcraft (Matthew B. Crawford) as another book that influenced my thinking.
One of my personal favorites is Pavement Paradise [2] documenting American parking spaces.
I'll also shamelessly plug some pictures of gas stations I took last summer :) [3].
[1] https://clui.org/photo-archive
To make a shameless plug, I'm working on a Python package called OpenATP [1] to make it easy to benchmark different models/harnesses for automated theorem proving. It supports running agents in Docker containers or Modal out of the box. If you try it out, I'd love to get your feedback!
I recently wrote about the surprisingly good performance I saw from Grok [2]. On more challenging proofs, Grok doesn't keep up with Opus/Fable and GPT 5.6. I was recently blown away by GPT 5.6 Sol. It's persistence in closing out proofs is unparalleled from what I've seen so far. OpenATP also supports Kimi and Leanstral [3], among others.
[1] https://github.com/henryrobbins/open-atp
TL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To make it easier to run/benchmark different models/harnesses, I created an open-source Python package called OpenATP [2]. I recently added support to use Grok 4.5 in the OpenCode harness as a prover and found it to be surprisingly competitive with Claude Code and Codex at a fraction the cost and wall-clock time.
- The OpenATP "standard provers" were used; see docs [5] for model / harness configuration details
- Time and cost are function of effort level, which may lead to unfair comparison across provers
- FATE-X excludes task 10 since claude and grok hit session limits
- FATE-X excludes leanstral and aristotle due to temporary endpoint failures
- Deepseek's FATE-X accuracy is corrected from 2 to 3 due to verifier bug (now fixed)
- 2 FATE-X deepseek misses are sorry-free, but rely on native_decide
- Claude's FATE-X miss is due to a failed delegation to a background subagent
- All costs come from underlying CLI, except codex which uses pricing table
I created this tool for my own research and have found it really helpful to benchmark different automated theorem provers (my experience so far has been that Claude Code + Codex still out-perform Leanstral). My genuine aim is to share that usefulness with others, not self promote!
Do you have that Labs setting enabled? When I contacted support, they said "enabling Labs models isn't available for self-serve activation on standard individual accounts." Do you have a different type of account?