I have PhD studentships available, and am always happy to chat about research. Feel free to reach out.

This website is a "forest" created using the Forester tool, a system of evergreen hypertext notes developed by, among others, Jon Sterling and Kento Okura. To search my forest, press Ctrl+K.

I believe LLMs and related Generative AI technologies are, in almost all cases, spiritually harmful and detrimental to human flourishing. And if that isn't bad enough, most of these technologies are controlled by harmful companies and deeply immoral people who massively contribute to human exploitation and environmental degradation. I refuse to use, conduct research on, or consume the output of any such systems. If you send me AI slop, I do judge you and I will think less of you. I am not interested in hearing any excuses for using the technology ("I only use it for..", "But it's okay if.."). If you feel compelled to say something like this to me, this is probably because deep down you know these technologies are harmful, both to you and to those around you, but you want to feel okay about how you use them. I will not grant you absolution. I do not use this technology, and neither should you.

• Domain theory
• Interactive theorem proving

See also Weeknotes