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.

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.

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.

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.

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.

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:

• A module for working with fully commutative elements in Coxeter systems (#30243).
• A new implementation of the Kazhdan–Lusztig basis of an Iwahori–Hecke algebra that allows computations that were previously slow or infeasible (#32352).

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

A collection of things too small for their own section:

• A playground and test-bed for Project Euler 208
• A schedule planner and visualizer for college schedules; create a link to share the schedule with others.
• A web component for displaying Smith charts.