Privacy

In effect from [DATE]. This is the first version of this page.

This page says what personal data Synthetic collects when you use synthetic.dev, why, who else receives it, how long it’s kept, and what you can ask us to do with it. It describes the service as it runs today, and changes as features ship (see Changes to this page).

Who we are

Synthetic is run by Synthetic LLC, of 202, Park Front Shinjuku, 2-8-15 Shinjuku, Shinjuku City, Tokyo 160-0022, Japan. Its representative is Rin Arakaki. We decide how your personal data is used. Under the General Data Protection Regulation (GDPR) of the EU, the UK and Gibraltar, that makes us its controller. Under Japan’s Act on the Protection of Personal Information (APPI), we’re the business handling it.

Rin Arakaki is responsible for how we handle personal data. Write to support@synthetic.dev, or call +81 90 6862 5422, about anything on this page.

What we collect, and why

Where the GDPR applies to you, each part below also gives the legal ground we rely on. How long we keep each kind of data is in How long we keep it.

Your account

• If you sign up with an email address: the address, which also serves as your account’s name.
• If you sign in with Google or GitHub: that account’s name, email address, profile picture link and id, and which of those details it lets us read. We show the picture in the app’s bar. The tokens it gives us at sign-in are used only to learn who you are, and we don’t keep them.
• If your account has a password: a hash of it. You set one when you sign up with an email address, or later through a password reset. We never store the password itself.
• Whether you’ve confirmed your email address.

We use these to create your account and sign you in, and you can’t have an account without an email address or a Google or GitHub account. Legal ground: providing the service you signed up for (GDPR Art. 6(1)(b)).

Other users can learn whether an email address has an account here: signing up with it says it’s taken, and sharing a document with it says whether an account has confirmed it. Legal ground: our legitimate interest in letting users sign up and share documents (Art. 6(1)(f)).

Signing in

Each sign-in starts a session. Your browser keeps the session’s key in a cookie, and we record the IP address and browser (its user agent) the sign-in came from. A session lasts 7 days, and is renewed at most once a day while you use it. Its record is deleted when you sign out, and when your password is reset or removed (see below).

We use this to keep you signed in, and to spot and stop misuse of an account. Legal grounds: providing the service, and our legitimate interest in keeping accounts secure (Art. 6(1)(f)).

If you forget your password, you can ask for a link that sets a new one. It works for an hour, and only once. We keep a one-way fingerprint of its code, with your account’s id. Resetting your password ends every session your account has. Legal ground: providing the service.

Whoever controls your account’s email address controls the account and everything in it, so sign up only with an address that’s yours. Once that address is confirmed, signing in with a Google or GitHub account that has verified the same address joins it to your account. If the account has a password, we delete it, end every session the account had, and email the address to say so: a password proves nothing about who owns an address, and the Google or GitHub sign-in does. If someone else had signed up with your address, anything they left in the account stays, and so does anything they shared from it with other users. You can delete conversations from the sidebar, delete documents from Documents and stop sharing them, and ask us to correct the account’s name (see your rights). Legal grounds: providing the service, and our legitimate interest in keeping accounts secure.

Your conversations with the agent

The agent is an AI system. When you ask it something, we store:

• your question, and when you asked it;
• its answer, with the reasoning the model returned along the way;
• what the agent read of a document to answer you, and what it wrote after reading it;
• which model answered, how many tokens it used and what it cost;
• any name you give the conversation, and your up or down votes on answers.

No other user can read your conversations, unless they control your account’s email address (see Signing in).

To answer, we send your question, the conversation’s earlier exchanges, anything the agent has read of a document for it, and our own instructions to Google’s Gemini API, which keeps them, and its answer, as who else receives your data says. We don’t send your name, email address or account. We don’t use your conversations to train AI models.

What the agent read of a document, and what it wrote after reading it, follow that document. While you can’t read the document, they’re hidden from you, and they come back if you can read it again. When part of the document is removed for good, or the document is erased, all of that goes, not only what used that part, though Google keeps what it was sent, as the table says. You can’t go on in a conversation that holds something hidden or removed, but you can start a new one, and you can still delete it. What you wrote yourself stays, and so does what you copied into another document.

We also keep a record of what each of your questions to the agent cost, and what they cost together each month, with the month and your account’s id, but nothing you wrote and no time of day. It stays when you delete a conversation, so we still know what your account spent that month.

Legal grounds: providing the service, and, for the record of what questions cost, our legitimate interest in keeping costs in check.

Tasks you give the agent

A task is work you hand the agent that takes longer than one answer. When you start one, we store:

• its goal, as you wrote it, and what you write to it later, such as a note when you retry a step;
• its plan, and what each step found, which the agent wrote;
• its runs, as we store a conversation’s;
• what happened to it and when: its steps, your pauses, resumes and cancels, its budget, and what it cost.

Only you can see your tasks, unless someone controls your account’s email address (see Signing in). To work on one, we send its goal, your notes, its plan and what earlier steps found, with our own instructions, to Google’s Gemini API, as for a conversation. Legal ground: providing the service.

Your documents

When you write a document in Synthetic, we store:

• what you write in it: a formula in each block, any proof in Lean you write of one, and its title, if you give it one;
• each change you make to it, with when you made it, your account’s id, and a random id for the browser tab it came from;
• its settings, and when you created it.

So a document keeps its history, including what you’ve removed from it.

You can share a document you own with another user, by the email address their account has confirmed, to read it or to edit it. They can read all of it, its history included: every earlier version, so also what you removed before you shared it, and when each change was made, with an id for the account that made it. What they copy stays where they put it, even after you stop sharing or delete the document. You see the email address of each user you share it with. No link opens a document to anyone you haven’t shared it with. Otherwise, no other user can read your documents, unless they control your account’s email address (see Signing in).

A document someone shares with you is theirs. They see your email address, and what you write in it joins its history, under your account’s id. It stays there while the document does, even after they stop sharing it with you. To have something you wrote there removed, ask its owner, or write to us.

If you own a document and allow it, in the chat’s menu or in Settings → Privacy, the agent can read it when you, or another user you share it with, ask a question from the chat’s dock beside it. It reads the document as it stands then, as text, such as its title, formulas and proofs, but not its history, up to 100,000 characters. It can also read the readings recorded of a formula: the committed one and your own, each as the Lean statement it means, with whether the formula still reads that way and whether one of your proof checks of it stands. What it reads goes to Google’s Gemini API, on the terms in who else receives your data, and again with each later question in that conversation. A document someone shares with you follows its owner’s answer, so what you write in it can go there too. A question asked anywhere else sends no document. If you paste part of one into a question, it goes with your question. We keep each answer you give on whether the agent may read your documents, with when you gave it, your account’s id and the version of the question you answered. We don’t use your documents to train AI models.

Legal grounds: providing the service, and, for what other users wrote in a document the agent reads, our legitimate interest in answering questions about it (Art. 6(1)(f)).

Checking your formulas with Lean

When you check a formula, you choose a reading of it, and Lean, the open-source prover, checks that it can state what that reading says. Once you’ve confirmed a reading, you can write a proof of it, and Lean checks the proof. Lean runs on our own servers at Google Cloud, so checking a formula or proof sends it to no other provider, though our logs can occasionally hold a fragment of it (see Server logs). We store:

• the reading you chose, with its block and the version of the document it was read in;
• if you own the document or can edit it, your commitment to the reading you check, which joins the document’s history with when you made it, your account’s id and the reading, and, if you withdraw it, when you did;
• each check of a reading or of a proof, and what Lean answered, its messages included;
• when you confirm that your formula and its reading say the same thing, your confirmation, which joins the document’s history with when you made it, your account’s id and the check it rests on, and, if you withdraw it, when you did.

Anyone who can read the document can see a commitment while it stands, with the reading it commits. Your confirmations stay in the document’s history, but only you can see them. Only you can see your other readings and your checks, and only while you can read the document. Legal ground: providing the service.

Monitoring the site

Our pages run Datadog’s browser monitoring. It records which pages you open and what they ask our servers for, where you click, how long pages take to load, the errors your browser runs into, with their messages, which can occasionally quote what you typed, your browser and device, and your IP address and the country, region and city it suggests. For one visit in ten, if you’ve agreed to it, it also records a replay of the page as you saw it. What you write, what you type, and what the pages show of your documents and conversations are masked, both in replays and in the names it gives your clicks. Our own labels, such as a button’s name, may not be. It keeps an anonymous id in a cookie for up to a year, to tell one visit from the next. We don’t send it your name or email address, or the link to your profile picture.

We use it to find and fix faults and slow pages. In the EEA and the EU’s territories, the UK, Gibraltar, Switzerland and Quebec, and wherever we can’t tell where you are, it asks first, and without your yes nothing is recorded: the legal ground there is your consent (Art. 6(1)(a)). Elsewhere it runs unless you turn it off. A replay needs your yes wherever you are. You can change your answer at any time in Settings → Privacy, which takes effect from then on. If your browser sends Global Privacy Control and you haven’t answered, we count that as a no and don’t ask you; you can still agree there yourself. An answer you’ve given stands until you change it. Your browser’s Do Not Track signal changes nothing here, since nothing on our site tracks you across other websites.

Server logs

Our hosting provider records each request’s address (URL), the page it came from, and its IP address and browser. It doesn’t record a request that carries a sign-in, email-confirmation or password-reset code. Our servers’ own logs record such a request without its code.

Our servers’ own logs, and the logs of the queues that hold their work for later, such as checks with Lean, record ids: of accounts, and of what’s in them, such as documents and checks. Our servers’ logs also record the IP address of a request refused for coming too often. Datadog receives our servers’ own logs, reports of a server’s crashes, and performance traces, which record each request’s address, with the secrets in its query masked, and its browser. We don’t set out to log what you write to the agent or in your documents, or what Lean answers when it checks your formulas. But when something fails, an error’s message can quote part of what it failed on, so these logs, reports and traces can occasionally hold a fragment of it.

We use these to run the service, keep it secure and fix faults. Legal ground: our legitimate interest in doing so.

Email

We send email through Resend, and only what using Synthetic needs: for example, the link that confirms your email address, the link that sets a new password when you ask for one, and a notice when signing in with Google or GitHub removes your account’s password. Legal ground: providing the service.

When you write to us or call us

When you write to us, to report content, make a complaint, act on your account or your purchase, or ask about your data, we keep your message and your email address, and your name if you give it. When you call us, we keep your number and a note of what you asked. We use them to answer you, and to act on what you ask or report. Legal grounds: providing the service, when you ask us to act on your account or your purchase (Art. 6(1)(b)); our legal obligations, such as acting on reports under the EU’s Digital Services Act (Art. 6(1)(c)); and otherwise our legitimate interest in answering you (Art. 6(1)(f)).

Authors named in the library

The library lists published papers and other works with their authors’ names, taken from the works themselves and from public records such as arXiv’s, HAL’s and the ACM Digital Library’s. Some authors also have a page that lists their works in the library, which search engines can find. For some, we also keep a link to a public profile, which the pages don’t show. Legal ground: our legitimate interest in a catalog of published mathematics. If you’re named there and want something corrected or removed, write to us.

Decisions about you

We make no decision about you by automated means alone that has legal or similarly significant effects.

Who else receives your data

These providers handle data for us, on our instructions and under contract:

• Google Cloud runs our servers and database in Japan, and keeps our servers’ and queues’ logs there, apart from those from before 26 October (see Data sent abroad), so it holds everything we store. Its error reporting also keeps a copy of the errors it finds in our servers’ logs, and may keep it outside Japan.
• Google’s Gemini API writes the agent’s answers. It receives your questions, the conversation’s earlier exchanges, what the agent reads of a document, your tasks’ goals, notes, plans and results, and our instructions, but not your name, email address or account. Google keeps what it’s sent, and what it answers, for 55 days, to check for abuse and for any disclosure the law requires, and its authorized staff may review it. It doesn’t train its models on it, apart from the models that enforce its policy. It doesn’t use what it’s sent to improve its products otherwise, and may store it in any country where Google or its agents have facilities.
• Temporal Cloud runs each answer and task step by step, on servers in Japan. It receives each one’s id and settings, with its size, cost and timing, but not what you write or what the agent answers.
• Datadog receives our servers’ logs, crash reports and traces, and the browser monitoring where it runs, on servers in Japan.
• Google Workspace hosts our email. It receives what you write to us, and may store it in any country where Google has facilities.
• Resend sends our email, from the United States. It receives your email address and the email we send you.
• Anthropic provides the AI tools we use to build and fix Synthetic. It receives what those tools read when we use them, such as our logs, traces and monitoring, and what we look at to fix a fault, and doesn’t train its models on it.

Other users receive what you share with them, and the owner of a document someone shares with you, and the others they share it with, see what you write in it (see Your documents). If you choose Google or GitHub to sign in, they tell us who you are, and handle your sign-in under their own privacy policies.

We give personal data to the police, a court or another authority only when the law requires it, or to protect someone’s life or safety. If something we learn suggests a crime that threatens someone’s life or safety, we tell the authorities that can act on it, as the EU’s Digital Services Act requires. Legal grounds: our legal obligations (Art. 6(1)(c)), and protecting someone’s life (Art. 6(1)(d)). If another organization takes over Synthetic, your data goes to it, and we tell you.

We don’t sell personal data, and we don’t share it for advertising. No other company collects information through our site about what you do on other websites.

Data sent abroad

We keep your data in Japan, apart from what Google’s error reporting, Google’s Gemini API, Google Workspace, Resend and Anthropic handle elsewhere, as listed above, and our servers’ and queues’ logs from before 26 October, which Google keeps outside Japan until the last of them are deleted on 25 November. The European Commission has found that Japan protects personal data adequately, and UK and Gibraltar law approve transfers to Japan on that finding.

Google, Datadog and Temporal are companies in the United States. They keep your data in Japan, but their staff, and the companies that help them, may reach it from the United States and other countries, for example to answer a support request. Resend keeps what it handles in the United States. Anthropic stores what it handles there, and may process it elsewhere too, such as in Europe, Asia and Australia.

For the data of users in the EEA and the UK, each of these providers has agreed to the European Commission’s standard contractual clauses, with the UK’s addendum to them. Google, Datadog and Resend are also certified under the EU-U.S. Data Privacy Framework and its UK extension, which also covers data from Gibraltar. Write to us for a copy of the clauses.

For users in Switzerland: Switzerland hasn’t found that Japan’s law protects personal data adequately, so we keep your data there, and send it to these providers, only as running the service you’ve asked for requires (Federal Act on Data Protection, Art. 17(1)(b)). Google and Datadog are certified under the Swiss-U.S. Data Privacy Framework, and Google, Datadog, Resend and Anthropic have agreed to the European Commission’s clauses as adapted for Switzerland.

While your data is in another country, that country’s courts, police and security agencies may be able to obtain it under its law.

For users in Japan: these providers are third parties in a foreign country under the APPI, even where their servers are in Japan. Each handles your data under a contract that requires it to protect your data as Japan’s law does. Ask us, and we’ll tell you how, and about each country’s rules (APPI Art. 28(3)).

How long we keep it

Deleting a conversation or a task removes it from our database at once. A document you delete stays, whole, for 30 days, so you can restore it from Recently deleted, and then we erase it. A deletion reaches our backups when they age out, 7 days after it reaches our database. We keep a record of each deletion, with only ids and times, so that restoring a backup can’t bring back what was deleted.

Closing your account deletes it, with your conversations, your tasks and your documents, deleted ones and what others wrote in them included, and your readings and checks wherever they are, apart from a reading you’ve committed in a document another user owns, with Lean’s checks of that reading. Those, and what you wrote or confirmed in such a document, stay in it, under your account’s id, which nothing we keep links to you once your account is gone. If something there names you, write to us. What other users’ conversations hold of your documents is hidden from them at once, and removed within about two days. Closing your account doesn’t delete what you’ve written to us, which we keep as the table says, or our logs, which age out. If we close your account ourselves, we keep what’s in it for 30 days after we close it, so you can ask for a copy, and, if you ask, until we’ve sent it.

Your rights

You can do some of this yourself: delete a conversation from the sidebar; delete a task from its page; delete a document from Documents, and restore it from Recently deleted for 30 days; stop sharing a document; and choose in Settings → Privacy whether Datadog’s monitoring records your visits, and whether the agent may read your documents.

Wherever you are, you can ask us for a copy of your personal data, in a form a computer can read, or to correct or delete it. Write to support@synthetic.dev from your account’s email address, or tell us how we can confirm the account is yours. We answer within a month, or 30 days if that’s sooner, and charge nothing. Where the law lets us take longer for a complex or repeated request, or refuse or charge for a plainly unfounded or excessive one, we tell you why, and where you can complain, within that time. To close your account, write to us the same way.

Under the GDPR (the EEA, the UK and Gibraltar), you can also ask us to restrict how we use your data, and to send the data you gave us to another service where we can. Where we rely on your consent, you can withdraw it at any time: that stops what it allowed from then on, and doesn’t make what we did before unlawful.

You can object. Where we use your data for our legitimate interests, such as keeping accounts secure, keeping our logs, answering you or listing the library’s authors, you can object at any time, for reasons about your own situation. We then stop, unless we have compelling grounds that override yours, or need the data for a legal claim.

Complaints. If you think we’ve mishandled your personal data, write to support@synthetic.dev. We confirm we’ve received your complaint within 30 days, look into it without undue delay, and tell you what we found and what we’ll do. You can also complain to the data protection authority where you live or work, or where you think the law was broken: in the UK, the Information Commission, in Gibraltar, the Gibraltar Regulatory Authority, and in Canada, the Office of the Privacy Commissioner of Canada.

Under the APPI (Japan), you can ask us to disclose the personal data we hold about you and our records of giving it to others, to correct it, and to stop using it or giving it to others (Arts. 33–35).

We don’t sell personal data. If you live in Nevada and want to tell us never to, write to support@synthetic.dev.

Age

You must be 18 or over to have an account. Anyone can browse the library without one. If we learn that an account’s holder isn’t old enough, we close the account (see How long we keep it).

Cookies and storage in your browser

The first three are needed for the site to work, so they’re set without asking.

The site also keeps these in your browser’s storage. The first three hold a choice you made, or what the chat’s dock needs to show the same conversation on every page, so they’re set without asking too:

Security

Data travels encrypted, over HTTPS. Only the people who run Synthetic, and the tools they use, can reach the database, through Google’s Identity-Aware Proxy. Users in Japan can ask us to describe our security measures in more detail (APPI Art. 32).

Changes to this page

Each version of this page says when it took effect. We post each new version here, with the date it takes effect. When a change is significant, such as to why we use your data, a new kind of recipient, who we are or how you can use your rights, we email you before it takes effect. Before we use data you’ve already given us for a new purpose, we tell you, and ask for your agreement where the law requires it.