38
91
158
|
Mentions
@
|
Stars | Project | Description |
|---|---|---|---|
| 55 | 3,763 | Lean 4 programming language and theorem prover | |
| 3 | 69 | Definitional implementation of Cedar language and utilities for DRT | |
| 1 | 52 | A formal consistency proof of Quine's set theory New Foundations | |
| 1 | 15 | Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel. |
Popular Lean Topics
Latest Mentions
Latest mentioned Lean repos
| Stars | Project |
|---|---|
| 3,763 | lean4 |
| 69 | cedar-spec |
| 15 | lean4checker |
| 52 | con-nf |
| 28 | lean-ssr |
| 197 | std4 |
| 7 | InfinitePrimes |
| 1,639 | mathlib |
| 5 | hatsugen |
| 837 | mathlib4 |
| 0 | LeanServer |
| 78 | symmetric_project |
| 46 | topos |
| 57 | logical_verification_2023 |
| 97 | logical_verification_2020 |
| 3 | lamda_calculus_formalizations |
| 322 | electrolysis |
| 195 | lean4-metaprogramming-book |
| 113 | lean4-raytracer |
| 0 | MyFirstProofInLean |
Latest Discoveries
Latest discovered Lean repos
| Stars | Project |
|---|---|
| 15 | lean4checker |
| 52 | con-nf |
| 28 | lean-ssr |
| 197 | std4 |
| 7 | InfinitePrimes |
| 0 | LeanServer |
| 78 | symmetric_project |
| 69 | cedar-spec |
| 46 | topos |
| 57 | logical_verification_2023 |
| 3 | lamda_calculus_formalizations |
| 195 | lean4-metaprogramming-book |
| 837 | mathlib4 |
| 0 | MyFirstProofInLean |
| 47 | lean-chat |
| 3 | exists-unique |
| 45 | flt-regular |
| 25 | mathematica |
| 32 | Functional-Benchmarks |
| 5 | hatsugen |
Recently updated posts
-
The Fermat's Last Theorem Project
-
Dafny is a verification-aware programming language
-
New Foundations is consistent – a difficult mathematical proof proved using Lean
-
LeanSSR: An SSReflect-Like Tactic Language for Lean
-
The Mechanics of Proof