"Type Theory and Formal Proof: An Introduction" book formalization in Lean

A Lean 4 formalization of partial combinatory algebras.

A Typst package to create Fitch-style natural deductions.

A formal verification of Linear PCP SNARKs.

Chess in Lean 4

Experiments in automation for Lean

Extism Lean4 Host SDK - easily run WebAssembly modules / plugins from Lean4 applications

LaTeX code for a paper on lean's type theory

A static analysis tool for Lean 4.

A project to map out the relations between different equational theories of Magmas.

Lean 4 formalization of Rubik's cubes

Formalization of communication complexity in Lean

An evaluation benchmark for undergraduate competition math in Lean4, Isabelle, Coq, and natural language.

A Library for Formally Verified Cryptographic Proof Systems

Examples using MetaProgramming for writing tactics etc.

Symbolic and Automatic Differentiation of Languages in Lean

A blueprint for a formalization of infinity-cosmos theory in Lean.

The Hitchhiker's Guide to Logical Verification and Associated Materials (2024 Edition)

コード例で学ぶ Lean 言語

Drawing commutative diagrams for Typst commute

Leaff is a diff tool for Lean environments

Visualizing the network of math theories.

A project to digitalise results from high energy physics into Lean.

Hadwiger-Nelson Problem Formalization in Lean 4

A Lean 4 Jupyter kernel via repl