“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? Can computer-aided proofs answer questions that pen-and-paper proofs are unable to answer?…