Docs Using the app
Welcome to Room to Prove
Room to Prove helps you read, write and explore mathematics and computer science.
- Lessons with figures you can play with.
- Proofs checked by Lean, and read back as mathematics.
- Python, exact computation and real references.
- An assistant, with the model you choose.
This help has two parts:
- Using the app: this page.
- Control and automate: what you, or an agent, can write and drive.
The window
| Where | What |
|---|---|
| Sidebar | lessons, drafts, the figure library, panels, theme |
| Page | what you are reading |
| Panels | TeX, Python, Plugins, Data, Assistant |
Show or hide a panel from the sidebar. Drag its left edge to resize it. Drag its title bar to float it.
Reading a lesson
- Figures move. Drag a point, move a slider, press play.
- Proofs are checked. A badge shows what Lean found.
- Names are links. Click a theorem or a word like "continuous".
- References are real. Each one comes from a public catalogue. See Where references come from.
A Lean block has five views:
- Read: the proof as mathematics.
- Steps: what is left to prove after each step.
- Step through: the same, hidden until you ask.
- Narrative: the proof as a paragraph.
- Source: the Lean itself.
Searching
Press ⌘K to search lessons, their Lean and all of Mathlib.
- Type a name, words like "mean value", or symbols like "a < b → a ≤ b".
- Click a result to open its page.
- ← Back returns to your search.
Press ⌘F to find words on the page.
Figures
- Open the Figure library: over a hundred figures.
- Filter by field, level and topic. Copy one into a lesson.
- Or ask the assistant to make one, or to change one.
- Keep your own in Your figures, next to the others.
Panels
- TeX: try a formula. Find commands by name.
- Python: run scripts with NumPy, SciPy, SymPy and Matplotlib.
- Plugins: add tools and libraries.
- Data: exact values, computed with Lean's rules.
- Assistant: ask about the lesson, or have it write a draft.
Your own lessons
- Under drafts, choose New, or Import… a file.
- Edit the Markdown, or double-click anything on the page.
- Each Lean block has its own Check button.
Setting up Lean
Lessons, figures, TeX and Python work right away.
Checking proofs and searching Mathlib need Lean. The first time a lesson needs it, the app tells you the size before downloading anything. The Lean line at the foot of the sidebar shows it any time.
Making it yours
- The palette at the foot of the sidebar picks a theme.
- The gear next to it sets the font, size, spacing and colours.
- ⌘=, ⌘− and ⌘0 zoom the window.
Keys
| Keys | Does |
|---|---|
| ⌘K | search |
| ⌘F | find on the page |
| ⌘= ⌘− ⌘0 | zoom |
| ⌘Enter | run, in Python |
| ⌘S | save, in the draft editor |
| Tab | next field of a template |
On Windows and Linux, use Ctrl for ⌘.
Control and automateOverviewEverything the app does, written as text you or an agent can drive.Control and automateLessonsMarkdown with formulas, numbered blocks, references, figures and Lean.Control and automateFiguresGraphs, geometry, animation and space, in a few lines.Control and automatePythonPlots, typeset formulas and tables from scripts.Control and automateLeanChecked proofs, declaration pages and search.Control and automateDataExact values and computations, with Lean’s rules.Control and automateFor agentsThe assistant: models, rules, and every tool it has.Control and automatePluginsTools, Python libraries and Lean libraries, yours or the catalogue’s.ArticlesHow Room to Prove reads LeanFrom the Lean you write to the mathematics you read.ArticlesWhere references come fromCitations from public catalogues: what works today, and what does not yet.AboutAboutVersion, privacy, acknowledgements and licence.