Awesome Lean / Libraries
18Scientific Computing & Machine Learning
19 entries
- SciLeanScientific computing: arrays, automatic differentiation and numerical methods.lecopivo/SciLean
- TorchLeanNeural networks with typed tensors, autograd, CUDA support and verification.lean-dojo/TorchLean
- TensorLibVerified tensor library.leanprover/TensorLib
- TablesDataframe library compatible with the B2T2 benchmark, with provable invariants.pandaman64/Tables
- HexVerified computational algebra: matrices, row reduction, polynomial factoring, LLL, graph isomorphism.leanprover/hex
- lpVerified linear programming solver that returns proof-carrying results, plus an
lptactic.leanprover/lp - LeanBLASBLAS bindings with specifications.lecopivo/LeanBLAS
- EigenLeanEigen linear algebra bindings.lecopivo/EigenLean
- NumLeanNumerical matrix computations.arthurpaulino/NumLean
- FloatLibVerified floating-point arithmetic across formats.
- FloatSpecFormally verified float implementation.Beneficial-AI-Foundation/FloatSpec
- fp-leanFloating-point semantics mechanization.opencompl/fp-lean
- LeanCertVerified interval arithmetic: bounds, root finding and optimization.alerad/leancert
- intervalConservative floating-point interval arithmetic.girving/interval
- lean-unitsSI physical unit system.ecyrbe/lean-units
- lean-autogradAutomatic differentiation following JAX's autodidax.alok/lean-autograd
- lean4-mlirNeural architectures specified in Lean, with verified GPU codegen.brettkoonce/lean4-mlir
- ginac-leanGiNaC computer algebra bindings.utensil/ginac-lean
- LeanSageCall SageMath from Lean.oOo0oOo/LeanSage