The mLab

A satire generator making fun of the nLab, a wiki for higher mathematics and category theory. Read about syntactically reflective presheaves or co-normally virtual limits, and follow links for more!

The main functionality is implemented in a standalone package nearley-generator which turns a Nearley parser grammar description into an efficient and customizable fake text generator.

Polyomino Solver

Solves arbitrary polyomino tiling problems, using different algorithms. The fastest such algorithm reduces the problem to exact cover and applies Algorithm X, which only finds exact solutions. Otherwise, there are methods to convert to SAT and solve via either a JavaScript SAT solver or a WebAssembly build of the Z3 Theorem Prover. The main UI functionality here is implemented as a web component web-component-polyomino.

Expand to see an example of a polyomino web component See the codepen demo for more!

Oracles Randomizer – Web

A web interface to the randomizer(s) for Legend of Zelda: Oracle of Seasons/Ages, which are originally command line programs written in Go. This web app runs the randomizer programs entirely in the browser by compiling them to WebAssembly and "emulating" a filesystem layer, as detailed here. This app provides access to three commonly used verisons of the randomizer in one location, by maintaining WASM binaries of all three.

OoTMM Checklist Tracker

A co-op capable checklist tracker for the OoTMM randomizer, that randomizes Legend of Zelda: Ocarina of Time and Majora's Mask together. Through WebRTC peer-to-peer connections, you and your co-op partners can keep track of all the checks and locations across both games, collaboratively editing the same checklist.

Manufactoria Editor

A modern re-skinned editor for levels in the classic flash game Manufactoria. Save and load programs from regular Manufactoria share URLs, and automate the verification of your programs running them against a test battery. Built in conjunction with @wkevina.

Just Track

A simple, offline, client-only time tracking app. Records and saves data locally in the browser, and past data can be viewed any time. Simple keyboard interface that supports assigning hotkeys and colors to tasks, with the currently tracked task being shown in the browser tab.

Genki DB

A small app to browser and filter over all the vocabulary and Kanji covered in the popular introductory Japanese textbooks, Genki I and II. Full offline support via PWA (progressive web app) functionality.


Lean is a programming language and interactive theorem prover out of Microsoft Research. I've contributed a few features to Lean's library of formalized mathematics:

  • A collection of results on lattice theory and order theory: #5825, #5871, #5942
  • A refactoring and simplification of existing proofs using the above results: #6082


SageMath is an open source mathematics software system. In some projects with Tianyuan Xu, we contributed some substantial features to SageMath:

In the future we also hope to contribute features for certain diagram algebras, which this small demo provides some pictures of.

Other Small Stuff

A collection of things too small for their own section: