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

61 stars written in Lean
Clear filter

Lean 4 programming language and theorem prover

Lean 6,879 715 Updated Dec 12, 2025

The math library of Lean 4

Lean 2,610 937 Updated Dec 12, 2025

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

Lean 1,666 293 Updated Jun 28, 2024

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 11, 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 136 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 11, 2025

Natural language tactics to teach mathematics using Lean 4

Lean 107 17 Updated Nov 23, 2025

**(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean.

Lean 101 21 Updated Oct 25, 2023
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 Nov 21, 2025

The Lean reference manual

Lean 90 41 Updated Dec 12, 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 Nov 24, 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

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

Lean 65 17 Updated Jul 18, 2024
Next