← All repos

SciLean

Scientific computing in Lean 4

GitHublecopivo.github.io/scientific-computing-lean/
lean4numerical-methodsscientific-computingsymbolic-computation
Browse cluster: Lean4 Formal Verification & Cryptography →
2,153commits
12contributors
7languages

Tech stack & purpose

SciLean is a library for scientific computing written in Lean 4, enabling users to solve differential equations, perform optimization, and build machine learning applications. The project aims to leverage Lean's expressive functional programming and formal mathematics capabilities to enable code transformation guided by mathematical formalization, symbolic computation as a first-class feature, code generation from formal specifications, and catalogization of numerical methods. SciLean is built in Lean 4 and relies on OpenBLAS for accelerating numerical computations, with support currently limited to Linux and macOS. The project is in early development and includes performance profiling examples comparing C reference implementations, optimized Lean implementations, and idiomatic SciLean code.

Community & reference links

Languages

Lean
99.8%
C
0.1%
Emacs Lisp
0.0%
Shell
0.0%
Makefile
0.0%
Dockerfile
0.0%
HTML
0.0%

Contributors