SampCert : Verified Differential Privacy

Formalizing stochastic doubly-efficient debate

Lean theorem proving interface which feels like pen-and-paper proofs.

Server to host lean games.

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

Tactics for discharging Lean goals into SMT solvers.

Python library for the Zulip API.

Zulip Desktop client for Mac, Windows and Linux.

Zulip mobile apps for Android and iOS.

Zulip server and web application. Open-source team chat that helps teams stay productive and focused.

Lean 3 material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

An implementation of Snakebird in Lean.

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

Lean 4 programming language and theorem prover

Emacs major mode for Lean 4

Cryptographic routines for the Lean 4 language

Basic Http functionality in Lean (unfinished)

A simple assertion command for Lean4

A Lean 4 library for iterators.

WIP unofficial package registry of Lean 4

SDL2 bindings for lean

Materials for the course "theorem prover lab: applications in programming languages" at KIT, SS2021 edition

Theorem Proving in Lean 4

Neovim support for the Lean theorem prover

Programming language for literate programming law specification

An embedding and formalization of GAP (groups, algorithms, Programming) in LEAN4