Agent

The agent is Synthetic’s AI assistant. You can discuss mathematical ideas, ask for examples, or put an argument into words for feedback. Its responses are generated by a model and can be mistaken.

Start a conversation

Open Chat and write a question. You can also open the chat dock while working in a Document and continue a conversation beside it. The dock and standalone chat share your conversations.

What the agent can see

Today the agent answers from the messages you write to it. Opening the dock beside a Document does not give the agent automatic access to that Document, and a general chat answer does not search the mathematical literature or run Lean.

If you want feedback on a formula or argument, include enough context in your message for the agent to understand the question. Do not treat an AI response as verified mathematical evidence.

Where to keep mathematics

Chat helps you explore an idea. Keep mathematical expressions and the work you want to revisit in a Document. To inspect an editor reading or understand what Lean checked, use the readings and checks guide.