Skip to content
View aresbit's full-sized avatar
💭
I may be slow to respond.
💭
I may be slow to respond.

Block or report aresbit

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

Starred repositories

23 stars written in Lean
Clear filter

Lean 4 programming language and theorem prover

Lean 7,935 828 Updated Apr 30, 2026

A Lean companion to Analysis I

Lean 1,689 230 Updated Apr 30, 2026

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

Lean 1,664 290 Updated Jun 28, 2024

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Lean 875 119 Updated Apr 30, 2026

Scientific computing in Lean 4

Lean 497 38 Updated Feb 18, 2026

Simple verification of Rust programs via functional purification in Lean 2(!)

Lean 341 7 Updated Mar 6, 2017

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

Lean 315 21 Updated Mar 9, 2024

Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.

Lean 251 59 Updated Mar 18, 2025

Theorem Proving in Lean 4

Lean 246 124 Updated Dec 19, 2025

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

Lean 216 46 Updated Mar 20, 2026

Source code for the Mathematics in Lean tutorial.

Lean 190 100 Updated Aug 20, 2025

Rewriting Principia Mathematica in Lean

Lean 137 1 Updated Feb 5, 2026

Hitchhiker's Guide to Logical Verification (2023 Edition)

Lean 115 19 Updated Nov 22, 2023

From Zero to QED: An informal introduction to formality with Lean 4

Lean 107 17 Updated Apr 20, 2026
Lean 79 6 Updated Apr 29, 2026

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

Lean 76 21 Updated Apr 14, 2026

A Cheat Sheet for Coq Developers who want to try LeanProver

Lean 19 1 Updated Jul 25, 2023

Supplement of the ICFP'22 paper "‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language"

Lean 14 2 Updated Feb 15, 2025
Lean 11 1 Updated May 14, 2023

Course repository for GlaMS - Formalising Mathematics in Lean (2024)

Lean 9 6 Updated May 13, 2024

Lean formalisation and textbook for Languages and Computation

Lean 2 Updated Oct 9, 2023

Hitchhiker's Guide to Logical Verification (2023 Edition)

Lean 1 2 Updated Jan 15, 2024