SciLean: 基于 Lean 的科学计算

一个用于科学计算的库，例如求解微分方程、优化或机器学习，使用 Lean 编写。该库处于早期开发阶段，在当前阶段仅是一个概念验证，展示如何使用 Lean 进行科学计算。

Lean 是一种表达力丰富的函数式编程语言，允许形式化这些计算背后的数学。这可以提供多种好处：

基于底层数学形式化的代码转换和优化，例如自动微分、代数简化、对所用近似值的精细控制或执行调度。
一等符号计算。任何函数都可以是纯符号的，像 gradient、integral 或 limit 这样的函数本质上不可计算。然而，它们承载了程序应执行的操作的含义，我们提供了工具来操纵它们或用实际可计算的函数来近似它们。
基于形式化规范的代码生成。许多科学计算或机器学习问题可以非常简单地表述，例如寻找函数的最小值点。然后我们提供工具将此类规范转换为满足规范的、通常在使用近似值的适当极限下的可运行代码。
数值方法的目录化。

简而言之，数学是数值计算的终极抽象，而 Lean 能够理解数学。希望借助 Lean，我们能够创建一个真正强大且可扩展的科学计算库。

文档

手册

Lean 中的科学计算
一本关于 Lean 中科学计算的进行中书籍。

演示文稿

Lean 中的自动微分 – Lean Together 2024 (30分钟)
Lean 中前向模式和反向模式自动微分的动机与示例。
Lean 中的科学计算 – Lean for Scientists and Engineers 2024 (2小时)
SciLean、n 维数组、符号计算和自动微分的概述。
Lean 中的科学计算 – 剑桥大学研讨会 (2024年5月9日)
涵盖通过微分方程进行优化、基础概率编程以及 Walk on Spheres 算法。

使用 SciLean

先决条件

SciLean 依赖 OpenBLAS 来加速数值计算。
你需要在系统中安装它：

Ubuntu:
```
sudo apt-get install libopenblas-dev
```
macOS:
```
brew install openblas
```
Windows: 目前未正式支持。

构建 SciLean

使用以下命令克隆并构建该库：

git clone https://github.com/lecopivo/SciLean.git
cd SciLean
lake exe cache get
lake build

使用 SciLean 设置您的项目

要在您自己的 Lean 项目中使用 SciLean：

为 scilean 添加一个 require 语句。
将 moreLinkArgs 设置为指向您的 OpenBLAS 库。

以下是一个名为 foo 的项目的示例 lakefile.lean：

import Lake
open Lake DSL System

def linkArgs :=
  if System.Platform.isWindows then
    panic! "Windows is not supported!"
  else if System.Platform.isOSX then
    #["-L/opt/homebrew/opt/openblas/lib", "-L/usr/local/opt/openblas/lib", "-lblas"]
  else -- Linux
    #["-L/usr/lib/x86_64-linux-gnu/", "-lblas", "-lm"]

package foo {
  moreLinkArgs := linkArgs
}

require scilean from git "https://github.com/lecopivo/SciLean" @ "v4.20.1"

@[default_target]
lean_lib Foo {
  roots := #[`Foo]
}

注意： 如果您的项目使用 mathlib，请确保与 scilean 版本兼容。或者，省略显式的 mathlib 要求，SciLean 会作为传递依赖引入一个兼容版本。