Documents

A Document is where mathematical work is kept. Today its page has an editable title and an ordered sequence of formula blocks. Each block has its own formula editor.

Create and reopen

Choose New Document to start, or open Documents to see your existing Documents. Writing in the empty block at the end creates a new one. You can move between blocks with the arrow keys at the top or bottom edge of a formula.

Pressing Backspace in an empty existing math block removes that block. Within a nonempty formula, Backspace edits the formula instead.

Saving

Changes are submitted after a pause in writing. The page also attempts to save when it loses focus or becomes hidden.

A rejected edit is not silently thrown away. The page shows the stored version and a notice with your change, allowing you to apply it again or discard it. A formula larger than the supported payload cannot be saved until you reduce it. The page warns before leaving when it knows there is unsaved work.

A Document’s save history and the editor’s local Undo are different: Undo operates on edits in the current formula editor. An update received from elsewhere can replace the local formula and start a new local Undo history.

What earlier blocks mean

Blocks are ordered, but an earlier formula block does not automatically introduce a definition or hypothesis for blocks below it. Do not rely on mathematical dependencies between adjacent blocks being inferred from their order.

Checking a formula

The margin beside a formula describes whether the user has confirmed a match with what Lean checked. That is not a statement that Lean proved the formula. See Readings and Lean checks for the distinction.

To learn how editing works inside one block, visit the formula editor reference.