-
-
LNSym Public
Forked from leanprover/LNSymArmv8 Native Code Symbolic Simulator in Lean
-
aesop Public
Forked from leanprover-community/aesopWhite-box automation for Lean 4
Lean Apache License 2.0 UpdatedJan 31, 2024 -
-
lean4 Public
Forked from leanprover/lean4Lean 4 programming language and theorem prover
Lean Apache License 2.0 UpdatedNov 7, 2023 -
-
mathlib4 Public
Forked from leanprover-community/mathlib4Work in progress mathlib port for lean 4
Lean Apache License 2.0 UpdatedFeb 7, 2022 -
book Public
Forked from rust-lang/bookThe Rust Programming Language
Rust Other UpdatedSep 10, 2021 -
alc-lean Public
Forked from arademaker/alc-leanFormalization of ALC Logic in LEAN Prover
Lean UpdatedFeb 9, 2021 -
lean Public
Forked from leanprover/lean3Lean Theorem Prover
-
-
Lean.tmbundle Public
Forked from leanprover/Lean.tmbundleA TextMate bundle for the Lean language
Apache License 2.0 UpdatedSep 25, 2016 -
leanproved Public
Forked from htzh/leanprovedTheorems proved using the Lean prover.
Lean UpdatedJul 1, 2015 -
isabelle Public
Forked from seL4/isabellegit mirror of the Munich isabelle hg repository
Isabelle Other UpdatedMay 27, 2015 -
-
-
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…
Coq GNU Lesser General Public License v2.1 UpdatedMar 5, 2015 -
-
presentations Public
Forked from leanprover/presentationslean-related presentations
HTML Apache License 2.0 UpdatedFeb 19, 2015 -
-
-
lean.js Public
Forked from leanprover/lean.jsLean ported to Javascript with Emscripten
Python UpdatedNov 5, 2014 -
leanprover.github.io Public
Forked from leanprover/leanprover.github.iowww
JavaScript MIT License UpdatedNov 5, 2014 -
TypeScript Public
Forked from microsoft/TypeScriptTypeScript is a superset of JavaScript that compiles to clean JavaScript output.
JavaScript Apache License 2.0 UpdatedOct 28, 2014 -
andromeda Public
Forked from Andromedans/andromedaA minimalist implementation of type theory, suitable for experimentation
OCaml UpdatedOct 25, 2014 -