LeanBSeries

A formalisation of Butcher series and Runge–Kutta order theory in Lean 4.

Building

Requires the sibling repository LeanRoughPaths (rooted trees and their Hopf algebras) checked out next to this one:

git clone https://github.com/daniil-shmelev/LeanRoughPaths lean-rough-paths
git clone https://github.com/daniil-shmelev/LeanBSeries    lean-b-series
cd lean-b-series
lake exe cache get
lake build