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 utilitiessample / 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.


  • LeanPlot.Demos.LinearDemoy = x
  • LeanPlot.Demos.QuadraticDemoy = x²
  • LeanPlot.Demos.CubicDemoy = 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.