Scientific Computing in Lean

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.

  1. 1. Working with Arrays
    1. 1.1. Basic Operations
    2. 1.2. Tensor Operations
  2. 2. Differentiation
    1. 2.1. Symbolic Differentiation
    2. 2.2. Automatic Differentiation
    3. 2.3. Function Transformation
  3. 3. Miscellaneous
    1. 3.1. Typeclasses as Interfaces and Function Overloading
    2. 3.2. Working with Quotients
  4. 4. Examples
    1. 4.1. Harmonic Oscillator
    2. 4.2. 🚧 Harmonic Oscillator Optimization