Lean
Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Lean 3's obsolete mathematical components library: please use mathlib4
Lean Library currently studying for a degree at Imperial College
Software Foundations using the Lean Theorem Prover
solutions in Lean to some exercises in Software Foundations
A little playground where I mostly complete tasks from Software Foundations in Lean.
Create the integers as equivalence classes from pairs of natural numbers.
A gamification of the theorems in MATH40002 Analysis 1
The Complex Number Game. Make the complex numbers in Lean.
Perfectoid spaces in the Lean formal theorem prover.
A library of results from Social Choice Theory, formalized in the Lean Theorem Prover.
Lean 4 programming language and theorem prover
A formal proof of the independence of the continuum hypothesis
Setup for autograding of Lean homework using GitHub Classroom
A sudoku game where you have to prove that your deductions are valid
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
My trials and tribulations involving Lean 4
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.