Learn Lean and topology

Interactive Coq Proofs in Vim

Bug-free machine learning on stochastic computation graphs

Some theorems presented to first and second year mathematics undergraduates, First and second year undergraduate level mathematics

Create beautiful, publication-quality books and documents from computational content.

Write C shims from within Lean code.

A collection of tools for writing technical documents that mix Coq code and prose.

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

A sudoku game where you have to prove that your deductions are valid

Building group theory from scratch in Lean

The Complex Number Game. Make the complex numbers in Lean.

Logic and Mechanized Reasoning

Animation engine for explanatory math videos

Theorem Proving in Lean 4

Python term rewriting

An equational theorem prover based on Knuth-Bendix completion

Lecture notes from Cambridge maths

Code for the manim-generated scenes used in 3blue1brown videos

A formalization of the Rubik's cube group

Formal to Formal Mathematics Benchmark

The Z3 Theorem Prover

Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.

The math library of Lean 4

Topological Data Analysis for Python🐍

Mathematical Components

💧 Liquid Tensor Experiment

Proving leftpad correct two-dozen different ways

A simple raytracer written in lean

Geometric Algebra for Python