Control and automate

Everything in Room to Prove can be written as text:

a lesson is Markdown;
a figure is a few lines;
a script is Python;
a proof is Lean.

Text can be saved, shared and generated. So you, or an agent, can drive the app with it.

Each page below starts simple. The full reference is at the end, made from the app itself.

The parts

Part	You write	You get	Page
Lessons	Markdown with maths	a numbered lesson	Lessons
Figures	a library name, or a few lines	a live figure	Figures
Python	a script	plots, formulas, tables	Python
Lean	a proof, or a link to one	a checked proof, in words	Lean
Data	values and sums	exact answers	Data
Assistant	a question	drafts, figures, scripts	For agents
Plugins	a folder	tools and libraries	Plugins

An example

A theorem in a lesson, linked to Mathlib:

Markdown

:::theorem[Mean value theorem]{#thm:mvt lean="exists_deriv_eq_slope" module="Mathlib.Analysis.Calculus.Deriv.MeanValue"}
If $f$ is continuous on $[a, b]$ and differentiable on $(a, b)$, some
$c \in (a, b)$ has $f'(c) = \frac{f(b) - f(a)}{b - a}$.
:::

The app checks the link with Lean, shows Lean's reading, and links to its page.

Addresses

Every page has an address. Use one as a link in a lesson: [the figure library](#/figures).

Address	Opens
`#/<pack>/<lesson>.md`	a lesson
`#/search`	search
`#/decl/<module>/<name>`	a declaration's page
`#/figures`	the figure library
`#/figures/<id>`	one figure, such as `#/figures/riemann_sum`
`#/figures/make`	the figure editor
`#/help/<page>`	a help page, such as `#/help/api-python`