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 supported. This note will be visible to only you.
Report abuse

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

Report abuse

Starred repositories

22 stars written in Lean
Clear filter

Lean 4 programming language and theorem prover

Lean 7,639 786 Updated Mar 24, 2026

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

Lean 1,664 292 Updated Jun 28, 2024

A Lean companion to Analysis I

Lean 1,625 217 Updated Mar 22, 2026

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

Lean 842 108 Updated Mar 24, 2026

Scientific computing in Lean 4

Lean 476 36 Updated Feb 18, 2026

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

Lean 340 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 314 21 Updated Mar 9, 2024

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

Lean 249 58 Updated Mar 18, 2025

Theorem Proving in Lean 4

Lean 243 122 Updated Dec 19, 2025

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

Lean 212 45 Updated Mar 20, 2026

Source code for the Mathematics in Lean tutorial.

Lean 185 97 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 114 19 Updated Nov 22, 2023

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

Lean 103 17 Updated Mar 22, 2026

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

Lean 74 19 Updated Mar 20, 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