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

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.

Documentation

• Simple plotting – #plot (fun x => x^2) just works with automatic axis labels and styling
• One-liner helpers – plot, plotMany, scatter, bar for beautiful plots with zero config
• Composable graphics – overlay or stack plots with the + operator
• Grammar of Graphics – fluent builder pattern inspired by ggplot2
• Faceting – multiple sub-plots in a grid layout
• Log/linear scales – visualize exponential growth with logarithmic axes
• Data transformations – apply scales, normalize, and smooth data

Add LeanPlot to your project's lakefile.toml:

[[require]]
name = "LeanPlot"
git = "https://github.com/alok/LeanPlot"

Then fetch and build:

lake update
lake build

You'll need node/npm on your PATH – ProofWidgets handles the bundling automatically.

import LeanPlot.API
import LeanPlot.DSL
-- Simple function plot
#plot (fun x => x^2)
-- With custom sample count
#plot (fun t => Float.sin t) using 400
-- Doc comments become chart captions (a poor man's legend!)
/-- The classic parabola y = x2 -/
#plot (fun x => x^2)
-- Multiple functions with automatic legend
#html plotMany #[("sin", fun x => Float.sin x), ("cos", fun x => Float.cos x)]
-- Scatter plot
#html scatter (fun x => x^2) (steps := 50)
-- Bar chart
#html bar (fun i => i^2) (steps := 10)

Hover over #plot or #html in VS Code to see the interactive charts!

import LeanPlot.API
import LeanPlot.Debug
open LeanPlot.API LeanPlot.Debug
#html withSavePNG (plot (fun x => x^2)) "my-plot" "quadratic.png"

import LeanPlot.Algebra
open LeanPlot.Algebra
#plot (
 line "y" (fun x : Float => x) +
 line "y2" (fun x => x*x)
)

import LeanPlot.GrammarOfGraphics
import LeanPlot.Core
open LeanPlot.GrammarOfGraphics
#html (
 plot (fun x => x * x)
 |> fun p => PlotBuilder.withTitle p "Quadratic Function"
 |> fun p => PlotBuilder.withSize p 500 400
 |> PlotBuilder.build
 |> Render.render
)

• LeanPlot.Demos.SmartPlottingDemo – Zero-config beautiful plots (start here!)
• LeanPlot.Demos.LinearDemo, QuadraticDemo, CubicDemo – Basic function plots
• LeanPlot.Demos.OverlayDemo – Overlaying multiple functions
• LeanPlot.Demos.TrigDemo – Trigonometric functions
• LeanPlot.Demos.LogScaleDemo – Logarithmic scales
• LeanPlot.Demos.GrammarDemo – Grammar of Graphics DSL
• LeanPlot.Demos.TransformDemo – Data transformations
• LeanPlot.Demos.FacetDemo – Grid layouts

Open any demo and hover over #plot or #html to see the charts.

Full documentation is available at https://alok.github.io/LeanPlot/

To build docs locally:

lake build leanplot-docs
.lake/build/bin/leanplot-docs
python3 -m http.server 8000 --directory _out/docs/html-multi

Apache License 2.0 – see LICENSE for details.