Lean 4 programming language and theorem prover

The math library of Lean 4

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

Demo for high-performance type theory elaboration

Scientific computing in Lean 4

Metamath Zero specification language

The "batteries included" extended library for the Lean programming language and theorem prover

Simple verification of Rust programs via functional purification in Lean 2(!)

White-box automation for Lean 4

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

Tactics for discharging Lean goals into SMT solvers.

💧 Liquid Tensor Experiment

Catalog Of Math Problems Formalized In Lean

Formalization of Mathematical Logic

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

Helper toolkit for creating your own Lean 4 UserWidgets

Experiments on automation for Lean

A simple raytracer written in Lean 4

Lean 4 kernel / 'external checker' written in Lean 4

A formal proof of the independence of the continuum hypothesis

Intuitive, type-safe expression quotations for Lean 4.

A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

Write C shims from within Lean code.

Ground Zero: Lean 4 HoTT Library

A quick reference for mapping Coq tactics to Lean tactics

Lean for the Curious Mathematician 2020

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

Topos theory in lean