JSON Schema in every programming language

plasTeX plugin to build formalization blueprints.

A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

The power of Claude Code / GeminiCLI / CodexCLI + [Gemini / OpenAI / OpenRouter / Azure / Grok / Ollama / Custom Model / All Of The Above] working as one.

Lean 4 proof verification without reference

Hosts the website for mathlib and other Lean community infrastructure.

The best ChatGPT that $100 can buy.

The Lean Computer Science Library (CSLib)

Formalisation of parts of the TC39 Temporal proposal in Rocq.

Lean Theorem Prover MCP

The JSON Schema specification

A minimal development of SSA theory

Scientific computing in Lean 4

The math library of Lean 4

RFC6265 cookie libraries for Racket

Faceted execution in Racket

Racket DSL for generating parsers from BNF grammars [moved to https://git.matthewbutterick.com/mbutterick/brag]

Preparatory Material for RacketFest

Chez Scheme

A self-hosting Scheme to WebAssembly compiler

A parallelism library for Common Lisp.

Utilities for working with XSL files.

Working with the XML forms of TPTP problems

Theory development with TPTP

Services for parsing Mizar texts

Web server written in Common Lisp

Emacs utilities to facilitate copyediting tasks at the Stanford Encyclopedia of Philosophy

My fink work

Breaking up mizar articles into bits and computing relations among them.

Licensing for the Mizar Mathematical Library