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

A project to digitalise results from physics into Lean.

Bug-free machine learning on stochastic computation graphs

LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

コード例で学ぶ Lean 言語

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

(Mirror) A Machine-to-Machine Interaction System for Lean 4

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

Materijali za radionicu interaktivnog dokazivanje teorema @ IS Petnica

monoidal categories in the Lean theorem prover

Extracting the semantics of Noir to Lean for formal verification

matroids in lean

Formalise Eudoxus reals in lean and prove they form a complete Archimedean ordered field.

Proof of soundness of the Unit-B refinement calculus

Step-by-step small or medium-sized projects in Lean

Formal verification of GT-SMDN framework in Lean 4. 53 theorems formalised, 28 complete proofs. Companion to 'Protecting Critical Infrastructure' book.

A Lean 4 eDSL for writing declarative, correct-by-construction packing lists for user defined expeditions (e.g. walking the Camino, hiking the CDT, dressing for a wedding)

Exercises from Theorem Proving In Lean

Formalization projects for the Foundation of Software course at EPFL

This project aims to formalize some concepts of Automata Theory and Parsing into Lean4 Theorem Prover. This was a course project for the course 'Proofs and Programs' offered by Prof Siddhartha Gadgil at IISc, Spring 2025.