For agents

The Assistant panel is an agent inside the app. It can:

• read the lesson you have open;
• search and read Mathlib;
• check Lean;
• write drafts, figures and scripts;
• work in your Python and Data panels.

Choose a model

Click the model badge at the top of the panel.

• On this computer: Ollama, LM Studio and others. Nothing leaves your computer.
• OpenRouter: sign in, then pick a model.
• Your own key: DeepSeek, OpenAI, Anthropic, Gemini and more.

Keys stay in your system's secret store.

Budget sets how long a reply may be, and how many steps it may take.

Try asking

• "Explain the proof of Theorem 3, step by step."
• "Find the Mean Value Theorem in Mathlib."
• "Write a short lesson on the Euclidean algorithm."
• "Make a figure of a Riemann sum with a slider for n."
• "Plot the first five Taylor polynomials of eˣ."

Keep an answer as a draft, then edit it.

The rules it keeps

• Its Lean runs in the sandbox, and Lean decides.
• Its figures are checked before you see them.
• Its references come from public catalogues.
• Its drafts are marked as its own until you edit them.

How it sees the app

Every tool answers in plain text:

• a figure, as what it draws;
• a Lean name, read as mathematics;
• a lesson, as its outline;
• a check, as a list of problems.

When a check finds a problem, the model fixes it and tries again.

Every tool

Made from the tools the panel gives the model:

The assistant has 26 tools.

Reading the lesson

The lesson open in the app: its outline, its blocks and its words.

doc_outline

The open lesson's outline: its title, sections, and every labelled theorem, equation, figure and code block, with the number the reader sees. Cite them in answers as @label (e.g. @thm:mvt).

No parameters.

doc_get

The source of one labelled part of the lesson (a theorem with its statement, an equation, a figure's DSL, a Lean block), by its label from doc_outline.

doc_search

Paragraphs of the lesson that contain some text (case-insensitive), each with the section it is in. Up to 6.

Figures

The figure library and the figure language: find, build, check and edit a figure.

figure_scenarios

List the figure library: known scenarios (graphs, Riemann sums, the unit circle, triangle centres, vectors, roots of unity, Taylor polynomials, Thales) with their parameters, and the reader's own figures (ids yours:…) that match. Start here before writing a figure from scratch.

figure_from_scenario

Make a figure from a library scenario. Returns its DSL (put it in a ```figure block), errors if any, and what it draws.

figure_reference

The figure language in one page: values (numbers, points, lists), marks, styles, blocks (def, for, if, group), timing, dataset producers and limits, with worked examples. Read it before writing a figure that no library scenario covers.

No parameters.

figure_check

Compile and evaluate figure DSL. Returns errors with line numbers, and what the figure draws. Use it on every figure you write before showing it.

figure_edit

Edit figure DSL by named statements and return the result, checked. Operations: {"op":"set","name":"A","statement":"point(1, 2) drag"} replaces what A is defined as; {"op":"add","statement":"segment(A, B) dashed"} appends a line; {"op":"remove","name":"A"} removes A's line; {"op":"view","statement":"view x -2..2, y -1..1 grid"} replaces the view.

Writing lessons, Lean and references

Drafts, the lesson checker, Lean in the sandbox, Mathlib, and citations from the catalogues.

lesson_reference

How a lesson is written in this app: title, sections (numbered by the app), theorem-like blocks and proofs, labels and references, maths, figures, Lean blocks and links to Lean. Read it before writing a lesson.

No parameters.

lesson_check

Check a lesson the way the app reads it: unknown labels and references, every figure compiled and run, every formula rendered, Lean blocks and the names they cite, statements linked to Lean. Give a draft id, or Markdown.

draft_write

Write a lesson into a draft the reader keeps (listed in the sidebar under drafts). Without an id: a new draft from this Markdown, which must start with "# Title"; returns its id. With an id: append this Markdown to the draft (append true, the default), or replace the whole draft (append false). Write a long lesson in parts, a section or two per call, then check it with lesson_check.

draft_read

A draft's Markdown, with line numbers, to revise it.

lean_check

Check a whole Lean file with Lean, in a sandbox, and read it back as the app reads Lean: Lean's errors with their lines, whether it is proved, and each declaration's statement in words. A file that declares an axiom, or uses sorry or native_decide, is accepted but not proved. Use it on every ```lean block before you give it, and give the code exactly as it checked. Import only the modules you need: all of Mathlib takes about 20 s.

mathlib_search

Search Mathlib and Lean core by words in names and docstrings, e.g. "mean value", "deriv eq slope", "compact image continuous". Returns up to 15 names with their kind, module and docstring. Search several times with different words; read a candidate with mathlib_decl before citing it.

mathlib_decl

One declaration as Lean reads it: its statement in words and TeX, its docstring, module, and the definitions and lemmas it uses. Takes a few seconds (Lean runs). Give the name and module from mathlib_search. A lesson block links to it with {#thm:x lean="Name" module="Module"}.

draft_edit

Change one part of a draft without rewriting it: {"id", "find", "replace"}. "find" must occur exactly once in the draft (give a few lines of context to make it unique). Use it to fix a formula, a figure line, a sentence or a Lean block; then check with lesson_check.

reference_list

A draft's bibliography: each key, the source, and where the app found it (a catalogue record), or "typed by hand, not checked".

reference_check

Check a draft's references against the catalogues (all of them, or one by its key): confirmed, differs (with what the catalogue has), or not found.

reference_search

Find a source in open catalogues (Crossref, arXiv, dblp, OpenAlex, Wikidata for books, Mathlib's bibliography) by words: authors, title words, year, e.g. "Cybenko 1989 sigmoidal". Returns records with their id. Never cite a source from memory: find it here, then add it with reference_cite.

reference_cite

Add a source to a draft's bibliography by its id from reference_search (a DOI, arXiv:…, W…, Q…, mathlib:…). The app fetches the record itself and returns the key to cite it with, as [@key] or [@key, p. 12].

Python and data

The reader’s Python and Data panels.

python_read

The reader's Python panel: its script, with line numbers, and the output of its last run (printed text, what it showed, the error). Read it before changing the script.

No parameters.

python_write

Put a whole script in the reader's Python panel and run it there; returns the output (printed text, what it showed, the error with its traceback). The reader's previous script comes back with Undo. Pyodide in the app, no network, no files: numpy, scipy, sympy, matplotlib are there (others only as the reader's plugins); show(x), show_tex(r"..."), show_html("...") display results. Never quote a number the run did not print.

data_reference

The data panel's language: how values are written (matrices, residues, Gaussian integers, quaternions, permutations…), the computations and functions, and Lean's rules it keeps (7 / 2 is 3 in ℕ). Read it before using data_add or data_compute.

No parameters.

data_read

The data panel's values for the lesson the reader is in: each name, its kind, its value, and where it came from.

No parameters.

data_add

Add a value to the data panel, as the reader would type it: {"name": "A", "value": "1 2; 3 4", "kind": "matrix", "over": "rational"}. The kind is guessed when omitted ("3 mod 7", "2 + i").

data_compute

Compute with the data panel's values, exactly, in the app, with Lean's semantics: "A * B", "A.det", "x ^ 6 = 1", "Nat.primeFactorsList 360". The result is added to the panel (under "name", or r1, r2…) and returned. Quote only results from here or from Lean.