Kyle Miller

lean4-raytracer. A simple raytracer written in Lean 4

LeanTeX. Lean 4 library for pretty printing expressions as LaTeX

knotfolio. A program for drawing knots and links, with support for importing images

textadv. An interactive fiction engine written in Python

zmach. A z-machine interpreter which does dynamic recompilation to javascript

LeanTeX-mathlib. LeanTeX pretty printers for mathlib

arrow_poly. Computation of (cabled) arrow polynomials of virtual knots

dcc. The Decaf Compiler Compiler

lean-graphcoloring. Using Lean to formalize proofs related to graph coloring

textadv-js. A pure-JavaScript interactive fiction engine that runs in the web browser

htmacros. Hypertext macros for managing websites using LaTeX-like syntax

msri2023_graphs. Repository for graph theory & combinatorics group at the MSRI Lean summer school

kmill.github.io. Professional website

planalg. Planar algebra computations in Mathematica

cse290q-25sp. CSE 290Q: Topics in Interactive Theorem Provers

squidlights. A general interface for light control

squidmusic. A distributed music system with remote speaker control

bignum.js. A library for doing arithmetic with big integers, rationals, and computable reals.

rts. JavaScript

nyc_address_extractor. Python

website. This is the source for my website

squidlights2. new udp-based squidlights

clangor. A language for sound synthesis

repl. A simple REPL for Lean 4, returning information about errors and sorries.

kmill-aoc2023. Advent of Code 2023

esplights. An "operating system" for the ESP8266 to control lights.

metaview. Python