Scientific Computing in Lean

🖨

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. Introduction
    1. Introduction
  2. Working with Arrays
    1. Basic Operations
    2. Tensor Operations
    3. Optimizing Array Expressions
  3. 🚧 Differentiation
    1. Symbolic Differentiation
    2. Automatic Differentiation
    3. Derivative Rules
    4. Differentiating Array Expressions
    5. Imperative and Monadic Code
    6. Variational Calculus
  4. 🚧 Function Transformation
    1. User Defined Function Transformation
    2. Expression Compiler
  5. Miscellaneous
    1. Typeclasses as Interfaces and Function Overloading
    2. Working with Quotients
  6. Examples
    1. Harmonic Oscillator