Lists (8)
Bag'o'tricks
Tools that just work28 repositories
Bleeding edge
What's the buzz? Tell me what's-a happening?10 repositories
Infrastructure
8 repositories
LOL
3 repositories
Mind of the Jedi
Codes that you got to learn from4 repositories
Personal Work
Ball 'n' Chains2 repositories
Pillar of Shame
3 repositories
Relic
Memories of the technological history8 repositories
Starred repositories
77
stars
written in Lean
Clear filter
Lean 4 programming language and theorem prover
Lean 3's obsolete mathematical components library: please use mathlib4
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
A project to digitalise results from physics into Lean.
Demo for high-performance type theory elaboration
The "batteries included" extended library for the Lean programming language and theorem prover
An introduction to theorem proving in Lean for the impatient.
Blueprint for the PNT+ Project
A verifier for automated and interactive proofs about transition systems.
Lean Library currently studying for a degree at Imperial College
A simple REPL for Lean 4, returning information about errors and sorries.
Lean 4 kernel / 'external checker' written in Lean 4
Definitional implementation of Cedar language and utilities for DRT
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.
A zero-knowledge Lean4 compiler and kernel
Interactive neural theorem proving in Lean
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.