The Julia Programming Language

⛓️ Simple verified compiler in Lean4. Lisp-like interpreter, simulated processor and correctness proofs.

Lean 4 programming language and theorem prover

Lean documentation authoring tool

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

The math library of Lean 4

The Sage Cell Server---providing a way to embed Sage computations into any web page.

Fermat's Last Theorem for regular primes

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

A library of results from Social Choice Theory, formalized in the Lean Theorem Prover.

👁 A merge bot for GitHub Pull Requests

Lecture notes, exercises, homeworks for Brown CS1951x 2021

The Lean version manager

💧 Liquid Tensor Experiment

Lean for the Curious Mathematician 2020

A formalization of the Rubik's cube group

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

Formalization of the existence of sphere eversions

Perfectoid spaces in the Lean formal theorem prover.

Lean-independent implementation of the MM-Lean link

Topos theory in lean

One direction of the MM-Lean link

System-wide Lean input method

A sudoku game where you have to prove that your deductions are valid