Getting started

In this walkthrough, you will create a Document, write a formula, save and reopen it, and inspect two possible mathematical readings. You do not need a Lean check to complete it.

1. Open a Document

Create a Document (you will need to sign in). Give it a title by typing in the title field. An empty math block at the end of the page says “Write mathematics”.

2. Write a formula

Try typing x + y. Spaces separate the three tokens on the current editor. The editor keeps the expression as written even before its meaning is chosen. The names are not yet declared to be types or natural numbers, so do not assume that either reading is a valid mathematical statement.

The toolbar inserts fractions, roots and scripts. Press Tab and Shift+Tab to travel between a structure’s slots. Typing ^ does not insert a superscript; use the Superscript button instead.

For the complete set of token and keyboard rules, see the formula editor reference.

3. Save and reopen your work

Look beside your edited math block for “Not saved yet”. Wait until that message disappears before leaving the Document: a brief pause alone does not confirm that the block reached the server. Then open Documents from the navigation and reopen the Document you just created. You should see the title and the formula you wrote. This is the first successful result of the walkthrough: your written mathematics survives reopening.

A title change is saved separately from a math block; allow it to save too. If “Not saved yet” does not clear, the block is too large to save, or Synthetic shows a refused-change notice, resolve the problem before leaving. Do not assume a pending or refused edit has reached the server.

For save conflicts and recovery, read working with Documents.

4. Inspect a mathematical reading

Place the caret in the sum and press Option+↑ (Alt+↑ off a Mac) until the whole sum is selected. Wait for the reading to appear beneath it. With the built-in notation, the first reading describes a sum of types; the line identifies it as reading 1 of 2. Press Tab to see addition of natural numbers, then Shift+Tab to return.

The two alternatives describe different possible meanings of the same written expression. The editor has not established whether the free names x and y have the required types.

The reading line gives you another observable result: the same written formula has two candidate structures. Neither reading establishes the types of the free names, and neither is itself a proposition that Lean can check as a theorem statement.

Continue with readings and Lean checks if you want to learn why the statement checker may decline a formula and what a successful correspondence would mean.

5. Ask the agent (optional)

Open Chat to discuss an idea or argument. The agent is an AI and can make mistakes. It does not automatically know the contents of your Document. Learn what the agent can do today.