Lessons

A lesson is Markdown, plus a few things for mathematics. The app numbers everything for you.

A first lesson

Markdown

# Curves

## Curvature {#sec:curvature}

:::definition[Curvature]{#def:curvature}
For a unit-speed curve $\gamma$, the *curvature* is $\kappa(s) = |\gamma''(s)|$.
:::

:::proposition{#prop:circle}
A circle of radius $r$ has curvature $1/r$ (see @def:curvature).
:::

:::proof
With $\gamma(s) = r(\cos(s/r), \sin(s/r))$, we get $|\gamma''(s)| = 1/r$.
:::

It reads like this:

Headings

# Title once, at the top.
## and ### for sections.
Add a label to refer to one: ## Curvature {#sec:curvature}.

Formulas

Inline: $e^{i\pi} + 1 = 0$ .
On their own lines: $$ \int_0^1 x^2 \, dx = \frac{1}{3} $$.
Numbered: put \label{eq:area} inside, and refer to @eq:area.

Try a formula first in the TeX panel.

Blocks

Write :::kind[Title]{#label}, the text, then :::.

Kind	Numbered
`theorem` `lemma` `proposition` `corollary`	yes
`definition` `example` `remark`	yes
`algorithm`	yes, on its own count
`proof` `note`	no

References

Refer to a label with @: @thm:mvt, @fig:secant, @eq:area.
It reads as "Theorem 3" or "Figure 2". Hover it to see the block.

Figures

Use one from the library by name:

Markdown

```figure {scenario="riemann_sum" f="sin(x)" n=8}
```

Or write your own. See Figures.

Algorithms

Markdown

:::algorithm[Binary search]{#alg:search}
```pseudocode
Search($a$, $x$)  // $a$ sorted
  $lo \gets 0$, $hi \gets |a|$
  while $lo < hi$ do
    $mid \gets \lfloor (lo + hi)/2 \rfloor$
    if $a_{mid} < x$ then $lo \gets mid + 1$ else $hi \gets mid$
  return $lo$
```
:::

Lean

Link a statement to Mathlib: add lean="name" and module="Module".
Show a Lean file: a lean block, or file="CollegeDemos/MeanValue.lean".

Python

A python block has Copy and Open in Python.

Citations

Cite as [@key], or [@key, Theorem 4.2].
Each key is a record from a public catalogue. See Where references come from.
The list of references is made for you.

Drafts

A draft is your own lesson, kept by the app.
Export saves it as an .rtp file to share.
Import… opens one.

At a glance

The summary the assistant reads, made from the app's own tables:

# Title once, at the top. Sections are ## Name {#sec:label} (and ###). The app numbers sections and blocks: never write numbers in headings or block titles.
Blocks: a line :::kind[Optional title]{#label}, the body, then ::: on its own line. Numbered together: theorem, lemma, proposition, corollary, definition, example, remark. Not numbered: proof, note, algorithm. A proof comes right after its statement as :::proof.
Labels and references: label prefixes thm: lem: prop: cor: def: ex: rem: alg: eq: fig: sec:; cite as @thm:x, @def:x, @sec:x, @fig:x. Every label you cite must exist.
Maths: $...$ inline, $$...$$ on lines of its own. Label an equation with \label{eq:x} inside $$...$$ and cite it as \eqref{eq:x}.
Link a statement or definition to Lean: :::theorem[Mean value theorem]{#thm:mvt lean="exists_deriv_eq_slope" module="Mathlib.Analysis.Calculus.Deriv.MeanValue"}. The app then shows Lean's own reading of it and a page for it. Link only a name you read with mathlib_decl, whose statement says what yours says; otherwise leave the block unlinked: the app marks it informal.
Figures: a ```figure {#fig:x caption="text with "} block in the figure language (figure_reference); check each with figure_check.
Lean: ```lean blocks, each a whole file (its own import and definitions). In a draft they are shown, never run: say they are unverified.
Citations: find a source with reference_search, add the one you mean with reference_cite (it returns the key), and cite it as [@key] or [@key, Theorem 4.2]. Never write a source from memory: one the catalogues do not have is named in words and said to be unverified.
Never quote a number that a figure or Lean does not compute.

A small example:

Markdown

# Curves

## Curvature {#sec:curvature}

:::definition[Curvature]{#def:curvature}
For a unit-speed curve $\gamma$, the *curvature* is $\kappa(s) = |\gamma''(s)|$.
:::

:::proposition{#prop:circle}
A circle of radius $r$ has curvature $1/r$ (see @def:curvature).
:::

:::proof
With $\gamma(s) = r(\cos(s/r), \sin(s/r))$, $|\gamma''(s)| = 1/r$.
:::