Stars
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
A project to digitalise results from physics into Lean.
The "batteries included" extended library for the Lean programming language and theorem prover
Tactics for discharging Lean goals into SMT solvers.
A verifier for automated and interactive proofs about transition systems.
A zero-knowledge Lean4 compiler and kernel
Formally Verified Arguments of Knowledge in Lean
Perfectoid spaces in the Lean formal theorem prover.
Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.
Intuitive, type-safe expression quotations for Lean 4.
A formalized proof of Carleson's theorem in Lean
Materials for the course "theorem prover lab: applications in programming languages" at KIT, SS2021 edition
A support library for working with zero knowledge cryptography in Lean 4.
This project contains various supporting libraries for lean to reason about protocols.
(Mirror) A Machine-to-Machine Interaction System for Lean 4
Extracting the semantics of Noir to Lean for formal verification
Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
A library of results from Social Choice Theory, formalized in the Lean Theorem Prover.
Unofficial repository for the experimental porting of mathlib into lean4