LeanPlot
LeanPlot turns Lean 4 code into interactive, React-powered charts that render right inside VS Code's infoview. Built on top of ProofWidgets4 and Recharts, it lets you inspect functions and data visually while you prove.
✨ Key features
- One-liner helpers
lineChart
/scatterChart
– produce a plot from a Lean function or an array of points with zero configuration. - Composable graphics algebra – overlay or stack plots with the
+
operator orPlotSpec.stack
. - Layered API – start at the high level and drop down to
PlotSpec
or the raw Recharts props whenever you need fine-grained control. - Sampling utilities –
sample
/sampleMany
uniformly sample any codomain that implements[ToFloat]
. - Demo gallery – ready-to-run examples under
LeanPlot/Demos
(linear, quadratic, cubic, overlay, stack, bar, area…).
🏗 Installation
Add LeanPlot to your project's lakefile.toml
:
[[require]]
name = "LeanPlot"
url = "https://github.com/alok/LeanPlot"
or to lakefile.lean
:
require LeanPlot from git
"https://github.com/alok/LeanPlot" @ "main"
Then fetch and build the deps:
lake update
lake build
(You'll need node
/npm
on your PATH – ProofWidgets handles the bundling automatically.)
🚀 Quick start
Create a new .lean
file, open the infoview, and paste:
import LeanPlot.Algebra
open LeanPlot.Algebra
#plot (
line "y" (fun x : Float ↦ x) +
line "y²" (fun x ↦ x*x)
)
Hover over #plot
and you'll see an interactive chart with two series.
🏟 Demo gallery
LeanPlot.Demos.LinearDemo
–y = x
LeanPlot.Demos.QuadraticDemo
–y = x²
LeanPlot.Demos.CubicDemo
–y = x³
LeanPlot.Demos.OverlayDemo
– overlay ofy = x
andy = x²
LeanPlot.Demos.StackDemo
– stacking via+
andPlotSpec.stack
Open any demo and hover the #html
command to run it.
🛠 Development
just build # lake build
just linter # run Std.Tactic.Lint (WIP)
just docs # regenerate docs (TBD)
Contributions welcome – check TODO.md
and open an issue or PR.
📄 License
LeanPlot is released under the Apache License 2.0; see LICENSE
for details.