computational origami library

E-values in Lean

How to say it using Mathlib.

Build structured Proof Blueprints with Verso

Lean 4 project focused on tactics that translate kernel equalities into categorical equalities, and back.

Scientific computing in Lean 4

Miscellaneous Developer Widgets for Lean

A project to digitalise results from physics into Lean.

jjui is a TUI designed for interacting with the Jujutsu version control system.

A basic Lean implementation of https://arxiv.org/pdf/2310.01530.pdf

A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.

Tree-sitter based s-expression navigation

Lean 4 port of Iris, a higher-order concurrent separation logic framework

Verified interval arithmetic for Lean 4 — prove bounds on exp, sin, cos, find roots, all machine-checked

Parser Combinator Library for Lean 4

Proétale cohomology in Lean

My personal website!!! (it's in Org mode!!!)

Majutsu! Magit for jujutsu

Reference compiler for c0

A Lean 4 companion to Lawvere and Schanuel's Conceptual Mathematics (2nd ed)

Visualize the undo tree.

COMPATibility Library for Emacs Lisp

A project for collecting and prioritising ideas related to tools, tactics, linters, code actions for Mathlib

A collection of reusable components from the Lean website designed build related sites with the same look and feel.

Lean documentation authoring tool

Formalization of Moreira's version of Sard's Theorem