Highlights
- Pro
-
SciLean Public
Scientific computing in Lean 4
-
-
gradbench Public
Forked from gradbench/gradbenchBenchmark for differentiable programming across languages and domains.
C++ MIT License UpdatedJan 8, 2025 -
-
scientific-computing-lean Public
work in progress book on Scientific Computing in Lean
-
lean-orbifolds Public
Forked from peabrainiac/lean-orbifoldsAn attempt at formalising the basics of diffeological spaces and orbifolds in the lean proof assistant.
Lean UpdatedNov 14, 2024 -
ReverseFFIwithMathlib Public
Example project for reverse FFI using Lean+mathlib
-
-
LeanColls Public
Forked from JamesGallicchio/LeanCollsWIP collections library for Lean 4
Lean Apache License 2.0 UpdatedAug 8, 2024 -
HouLean Public
Lean 4 as a scripting language in Houdini
-
sphere-eversion Public
Forked from leanprover-community/sphere-eversionFormalization of the existence of sphere eversions
-
-
lean4 Public
Forked from leanprover/lean4Lean 4 programming language and theorem prover
Lean Apache License 2.0 UpdatedNov 15, 2023 -
-
-
-
-
SciLeanExamples Public
SciLean examples mainly running through widgets
-
WidgetKit Public
Forked from leanprover-community/ProofWidgets4Helper toolkit for creating your own Lean 4 UserWidgets
Lean Apache License 2.0 UpdatedNov 16, 2022 -
openvdb_dev Public
Forked from sideeffects/openvdb_devOpenVDB Development Repository
C++ Mozilla Public License 2.0 UpdatedSep 28, 2022 -
lean4-mode Public
Forked from leanprover-community/lean4-modeEmacs major mode for Lean 4
Emacs Lisp Apache License 2.0 UpdatedMar 19, 2022 -
-
-
mathlib4 Public
Forked from leanprover-community/mathlib4Work in progress mathlib port for lean 4
Lean Apache License 2.0 UpdatedDec 9, 2021 -
wolfram-mode Public
Forked from kawabata/wolfram-modeEmacs editing mode for Mathematica and inferior shell.
-
-
mathlib Public
Forked from leanprover-community/mathlib3Lean mathematical components library
Lean Apache License 2.0 UpdatedNov 3, 2020 -
-
math-classes Public
Forked from coq-community/math-classesA library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]
Coq Other UpdatedOct 29, 2019 -
UniMath Public
Forked from UniMath/UniMathThis coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Coq Other UpdatedOct 17, 2019