LeanPlot

Line y = x Quadratic y = x² Overlay of y = x and y = x²

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 or PlotSpec.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 of y = x and y = x²
LeanPlot.Demos.StackDemo – stacking via + and PlotSpec.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.

LeanPlotv0.1.0