Skip to content
View brendanzab's full-sized avatar
πŸ˜΅β€πŸ’«
writing elaborators
πŸ˜΅β€πŸ’«
writing elaborators

Sponsoring

@servo

Organizations

@yeslogic @PistonDevelopers @gluon-lang @proglangdesign @pikelet-lang

Block or report brendanzab

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

πŸ“½ Animation

5 repositories

πŸ–ΌοΈ Art

3 repositories

πŸ“œ Binary Formats

55 repositories

πŸŒ€ Bootstrapping

49 repositories

πŸ—οΈ Build systems

11 repositories

πŸ“ Compilation

31 repositories

🎨 Creative Tools

37 repositories

πŸ—„ Data Layout

3 repositories

Starred repositories

55 results for source starred repositories written in Lean
Clear filter

Lean 4 programming language and theorem prover

Lean 6,878 715 Updated Dec 13, 2025

The math library of Lean 4

Lean 2,612 941 Updated Dec 13, 2025

Demo for high-performance type theory elaboration

Lean 572 28 Updated Oct 24, 2023

Scientific computing in Lean 4

Lean 441 36 Updated Jun 9, 2025

Metamath Zero specification language

Lean 364 48 Updated Dec 8, 2025

White-box automation for Lean 4

Lean 319 45 Updated Dec 13, 2025

Tactics for discharging Lean goals into SMT solvers.

Lean 240 31 Updated Nov 19, 2025

A minimal development of SSA theory

Lean 202 23 Updated Dec 12, 2025

A verifier for automated and interactive proofs about transition systems.

Lean 163 9 Updated Nov 28, 2025

Experiments on automation for Lean

Lean 148 24 Updated Dec 4, 2025

A simple raytracer written in Lean 4

Lean 143 5 Updated May 16, 2024

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

Lean 137 14 Updated Dec 8, 2025

A formal proof of the independence of the continuum hypothesis

Lean 136 16 Updated Aug 26, 2024

Lean 4 port of Iris, a higher-order concurrent separation logic framework

Lean 134 22 Updated Dec 8, 2025

Perfectoid spaces in the Lean formal theorem prover.

Lean 128 14 Updated Jul 9, 2024

Document Generator for Lean 4

Lean 113 57 Updated Dec 13, 2025

Natural language tactics to teach mathematics using Lean 4

Lean 107 17 Updated Nov 23, 2025
Lean 93 9 Updated Nov 12, 2023

A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

Lean 93 21 Updated Dec 13, 2025

The Lean reference manual

Lean 90 41 Updated Dec 13, 2025

HoTT in Lean 3

Lean 82 12 Updated Aug 3, 2020

tool for turning Lean proofs into Blender animations

Lean 78 6 Updated Dec 2, 2025

A formal consistency proof of Quine's set theory New Foundations

Lean 75 8 Updated Jun 18, 2025

Ground Zero: Lean 4 HoTT Library

Lean 73 3 Updated Dec 13, 2025

A quick reference for mapping Coq tactics to Lean tactics

Lean 71 4 Updated Apr 23, 2021

Lean for the Curious Mathematician 2020

Lean 68 75 Updated Oct 24, 2023

Topos theory in lean

Lean 64 2 Updated Jan 6, 2021

Experiments with SAT solvers with proofs in Lean 4

Lean 62 3 Updated Jun 23, 2024

M4 algebraic geometry course in Lean

Lean 58 5 Updated Mar 4, 2020
Next