Scientific Computing in Lean
Introduction
1. Sorry Friendly Programming
2. Setting Up Lean and SciLean
Working with Arrays
1. Basic Operations
2. Tensor Operations
3. Optimizing Array Expressions
4. Abstract Array Interface
Differentiation
1. Zoo of Differentiation Operators
2. Defining New Functions
3. Theoretical Aspects*
Function Transformations
1. Defining New Function Transformation
2. Function Transformation Algorithm*
Problem Transformations
1. Solve Function
2. Approximation
Differential Equations
Probabilistic Programming

Scientific Computing in Lean

by Tomáš Skřivan

Work in progress book on using Lean 4 as a programming language for scientific computing. Also serves as reference for SciLean library.

This book in its current form is a draft and is subject to change. Code might not work, explanations might be incomplete or incorrect. Procced with caution.

Release history

March, 2024

At the beginning there was nothing.

License

This work is licensed under a Creative Commons Attribution 4.0 International License.