“Look between the stars for what you need. The untraceable black of the possible…What does it mean to listen darkly?” (Healing Justice Lineages)

Other Formats

I gave a talk about Starling which you can watch on Vimeo .

The writing in this post is also available in a the format of a zine .

What is a Proof Assistant?

A proof assistant is a programming language and/or user interface that enables the creation of computer-aided proofs. Proof assistants are interactive theorem provers.

The subject of this article, Starling, is a proof assistant designed for ease of use by novices.

If this terminology confuses you, my expository talk might be helpful.

Why another proof assistant?

I was in a directed reading program for number theory which opened my eyes to the importance of proofs in mathematical discovery.

What do the proofs of the future look like?…