What is Synthetic?

Synthetic is a working environment for mathematics. Rather than treating a formula only as text to typeset or as code in one proof assistant, it keeps what you wrote and lets you inspect possible mathematical readings separately.

You can write an unfinished expression, return to it later and explore the structure that the notation reader recognizes. A possible reading is not yet a claim that the expression is well-typed, meaningful in every context or true.

Why work this way?

Mathematical research moves between tentative notation, chosen meaning, conjectures and justification. TeX expresses written notation, Lean checks formal work in its own language, and an AI conversation can help explore ideas. Synthetic aims to keep these activities connected to revisable mathematical work, without treating what was written, what was intended and what was checked as interchangeable.

Today that connection reaches Documents, candidate readings, and correspondence checks for a restricted set of statements. Shared mathematical operations for people and the agent, proof checking and adoption of proposed changes are still being built. The purpose of the separation is to make those future operations inspectable rather than silently trusting a generated interpretation or answer.

What you wrote, what it means, what is checked

These are distinct stages of working with a formula:

1. Writing. The Document stores the expression you authored, including presentation structures such as fractions and scripts.
2. Reading. Synthetic recognizes candidate mathematical structures from supported notation. A formula can have different readings or unfinished parts.
3. Choosing and checking. When the editor offers alternatives, you can choose one and request a Lean correspondence check. Synthetic shows what was sent, what came back and whether a faithful check was possible.
4. Evidence. Confirming that Lean checked the statement you intended does not mean a theorem has been proved. A proof needs additional evidence, which this current workflow does not produce.

For example, x + y may describe addition of natural numbers or a sum of types in the built-in notation. Without knowing what x and y denote, that choice is not a proof or a successful type judgment. The distinction between the symbols on the page and their possible interpretations is intentional.

Documents and the agent

A Document is where your written mathematics persists. The agent chat is a separate conversational interface for discussing ideas and arguments. Currently, placing chat beside a Document does not automatically give the agent access to its mathematical contents. An AI answer is not a checked mathematical result.

What Synthetic does not yet do

The present editor reads a built-in collection of mathematical notation rather than arbitrary notation declared by each Document. Earlier blocks do not automatically become definitions for later blocks. The current Lean integration checks correspondence of supported statements but does not construct proofs or accept agent proposals as mathematical contributions.

The longer-term goal is for people and the agent to work on mathematical objects through shared, inspectable operations while keeping proof authorities responsible for their own judgments. That is a product direction, not a feature available in the present interface.

Try it

Continue with the first Document walkthrough. It shows how to enter a formula, save and reopen it, and inspect two possible readings. Checking a statement with Lean is a separate task.