Lean 4 programming language and theorem prover

The math library of Lean 4

Scientific computing in Lean 4

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Tactics for discharging Lean goals into SMT solvers.

blueprint for prime number theorem and more

A simple raytracer written in Lean 4

Lean documentation authoring tool

Helper toolkit for creating your own Lean 4 UserWidgets

A formal proof of the independence of the continuum hypothesis

Catalog Of Math Problems Formalized In Lean

Benchmark for undergraduate-level formal mathematics

A simple REPL for Lean 4, returning information about errors and sorries.

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

Experiments in automation for Lean

Intuitive, type-safe expression quotations for Lean 4.

HoTT in Lean 3

数学系のためのLean勉強会

Code samples for Lean 4

Document Generator for Lean 4

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

A formal consistency proof of Quine's set theory New Foundations

Mathlib search tool

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

コード例で学ぶ Lean 言語

Topos theory in lean

A static analysis tool for Lean 4.

Experiments with SAT solvers with proofs in Lean 4