Readings and Lean checks

Synthetic keeps the formula you wrote separate from its possible mathematical meanings. The notation reader can recognize structure without rewriting the original formula or proving that a particular reading is correct.

Explore a reading

For example, A + B can be read as a sum of types or as addition of numbers, depending on the meaning of its parts. The line under the formula shows the reading of a selected part and, when relevant, that other readings exist.

• Option+↑ (Alt+↑ off a Mac) selects a larger mathematical part; Option+↓ goes inward.
• Option+← and Option+→ move to neighboring parts.
• Tab and Shift+Tab cycle a selected part’s alternative readings.
• Enter chooses the reading shown when the selected part offers alternatives.
• Escape ends structural selection and returns to the earlier caret or selection.

A formula with missing pieces remains editable. Finish it before choosing among its mathematical readings. A subsequent edit ends the current choice.

Try a reading

In a Document, type x + y and leave the caret in the sum. Press Option+↑ (Alt+↑ off a Mac) until the sum is selected. Its built-in notation offers a sum of types and addition of natural numbers as possible readings. Press Tab to compare them, then Enter to choose the one shown. If checking is available, the panel shows whether the selected reading could be checked with Lean and what statement was sent. A candidate reading is not automatically a valid or proved theorem.

This example is for choosing a reading, not for obtaining a successful Lean correspondence. Both the sum-of-types and natural-number-addition readings are non-propositions, and the names have no declarations in the current Document context. The statement checker can decline to send them to Lean; that is an expected limitation, not a failed proof.

Checking with Lean

Where the checking service is available and Synthetic can express the chosen reading faithfully in Lean, choosing a reading asks for a check. The panel can show the expression as written beside the statement sent to Lean, as well as Lean’s answer or why no check could be made.

Read the comparison carefully. “They agree” records your confirmation that the statement sent to Lean matches the reading you intended. “They differ” moves to the next available reading, just as Tab does: it does not record a disagreement or claim that Lean is mathematically wrong. A check may also be refused, incomplete, or have unresolved obligations.

Confirming a match is not proving a theorem. A well-formed statement checked with its proof left as an obligation is not an established result. A mathematical claim needs appropriate proof evidence before it can be treated as proved.

Limits

The current notation reader starts with a built-in collection of symbols and meanings; it does not yet use arbitrary notation declared by your Document. Not every mathematical reading can be expressed faithfully in Lean. A Lean check speaks only for the statement actually sent to Lean, not automatically for every possible meaning of the original formula.

For input rules and structural shortcuts, see the formula editor reference. To return to the editor, open your Document.