Draw flows (migration, goods, money, information) on ggplots.

Mojo Bindings for DuckDB

Implementations of algebraic rewriting techniques like DPO, SPO, SqPO.

The code used to create and update the Open Australian Legal Embeddings, the first open-source embeddings of Australian legislative and judicial documents.

The code used to create and update the Open Australian Legal Corpus, the first and only multijurisdictional open corpus of Australian legislative and judicial documents.

The Mojo Programming Language

Chat With All Kinds of AI Models Through a Common Interface

Lean theorem proving interface which feels like pen-and-paper proofs.

LLM inference in C/C++

Scientific computing in Lean 4

Algebraic graphs in R

My NixOS configurations.

Simple and Distributed Machine Learning

Discrete-Event Simulation for R

Building Blocks for Quantile Functions

The user home repository for the Mathematics in Lean tutorial.

Developer environments you can take with you

math puzzles from various sources, formalized in Lean

A clean interface for org files (Emacs)

Lean 3's obsolete mathematical components library: please use mathlib4

R package: generate best-practice stats spreadsheets for publication

GPT RStudio addins that enable GPT assisted coding, writing & analysis

Tutorials and sampling algorithm comparisons

Port of OpenAI's Whisper model in C/C++

A simple gtk4/libadwaita software center to easily install and manage nix packages

Extended two-way fixed effects

R extension library for rust designed to be familiar to R users.

Very controlled natural language tactics for Lean