The math library of Lean 4

Lean 4 programming language and theorem prover

The Z3 Theorem Prover

The agda-unimath library

Development of homotopy type theory in Agda

A new Categories library for Agda

An experimental library for Cubical Agda

The Agda standard library

Agda is a dependently typed programming language / interactive theorem prover.

A Learning Environment for Theorem Proving with the Coq proof assistant

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

agda-mode for neovim

A Rust/WASM implementation of homotopy.io

Neovim support for the Lean theorem prover

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Programming Languages Zoo

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

White-box automation for Lean 4

The Lean 4 web editor

The "batteries included" extended library for the Lean programming language and theorem prover

Visual Studio Code extension for the Lean 4 proof assistant

Document Generator for Lean 4

The Lean version manager

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

Natural Number Game

Server to host lean games.

Helper toolkit for creating your own Lean 4 UserWidgets

Mathlib search tool

Tool for data extraction and interacting with Lean programmatically.

plasTeX plugin to build formalization blueprints.