Why

Mathematicians and computers do not work with mathematics in the same language.

Our hypothesis is that there can be a sufficiently simple and consistent representation of mathematics, informed by homotopy type theory, that mathematicians want to work with directly, and whose structure computers can operate on.

If this hypothesis is false, there is no Synthetic.

Open Synthetic

What

Work with mathematics.

What you see as mathematical notation, Synthetic understands as mathematical structure.

A map out of a sum is a pair of maps:

(A + B \to C) ≃ (A \to C) \times (B \to C) .

Function type

from $A + B$ to $C$ , on the left side of an equivalence

Name the argumentDeleteMore

Preview $(: A + B) \to C$

Enter apply Esc cancel

Notation

$(A + B \to C)$

$≃ (A \to C) \times (B \to C)$

What you write.

Diagram

Two triangles that commute.

Count

$| A | = 1, | B | = | C | = 2$

$2^{1 + 2} = 2^{1} \cdot 2^{2}$

$8 = 2 \cdot 4$

Counting the maps between finite sets.

Geometry

Two points into an interval: the square, as two triangles.

One object, many ways of seeing it. Views beyond notation are in development.

How

An agent to read, understand and build mathematical knowledge.

We are building an AI agent that works with mathematics: reading existing literature, reconstructing results in our representation, connecting them, checking them where possible, and collaborating with mathematicians to extend what is known.

Humanwrite · explore · ask · accept

Same mathematical objects

Agentread · search · reason · propose · verify

From the literature

Categories for the Working Mathematician

IV.6 Cartesian closed categories

hom (a \times b, c) ≅ hom (a, c^{b})

reconstructed

Proposed by the agent

(A \times B \to C) ≃ (A \to (B \to C))

Reconstructed from: Mac Lane, Categories for the Working Mathematician, 1971
Related results: currying, exponential law, adjunction
Formal counterpart: Mathlib, Equiv.curry
Checked: Not yet

AcceptEditDiscardSources and details

An illustration of work in progress: the agent doesn’t reconstruct results from the literature yet.

Find related results.

Search by intent, not by infrastructure. Results will span our library, formal mathematics and indexed papers, and always say where they looked.

Searched: Synthetic Library, Mathlib, indexed papers
Not searched: the web

Verify

Know what has been checked.

Every statement carries its status. Checked means a formal proof checker accepted it; anything else says what it is.

$(A + B \to C) ≃ (A \to C) \times (B \to C)$: Checked
$(A \times B \to C) ≃ (A \to C) \times (B \to C)$: False

Build

A growing body of mathematical knowledge.

Results are connected, attributed and citable, and available to both humans and machines, with their sources and formal counterparts attached.

Search and verification are in development. The library is open today.

(A + B \to C) ≃ (A \to C) \times (B \to C)

(A \times B \to C) ≃ (A \to (B \to C))

Mathlib: Equiv.curry

hom (a \times b, c) ≅ hom (a, c^{b})

Mac Lane, 1971

c^{a b} = {(c^{b})}^{a}

(A \to B \times C) ≃ (A \to B) \times (A \to C)

Mathlib: Equiv.arrowProdEquivProdArrow

{(b c)}^{a} = b^{a} c^{a}

(A \to B + C) ≃ ?

c^{a + b} = c^{a} c^{b}

(𝟎 \to C) ≃ 𝟏

A \times (B + C) ≃ A \times B + A \times C

(𝟏 \to C) ≃ C

Mathlib: Equiv.sumArrowEquivProdArrow

Synthetic Library: type theory, sum types

sourcecounts tonullary caseas hom-setscounts tocounts toand into a sum?

$(A + B \to C) ≃ (A \to C) \times (B \to C)$ ; Mathlib: Equiv.sumArrowEquivProdArrow; source: Synthetic Library: type theory, sum types
- counts to: $c^{a + b} = c^{a} c^{b}$
- nullary case: $(𝟎 \to C) ≃ 𝟏$
- $(𝟏 \to C) ≃ C$
- $A \times (B + C) ≃ A \times B + A \times C$
- $(A \times B \to C) ≃ (A \to (B \to C))$ ; Mathlib: Equiv.curry
  - as hom-sets: $hom (a \times b, c) ≅ hom (a, c^{b})$ , Mac Lane, 1971
  - counts to: $c^{a b} = {(c^{b})}^{a}$
- $(A \to B \times C) ≃ (A \to B) \times (A \to C)$ ; Mathlib: Equiv.arrowProdEquivProdArrow
  - counts to: ${(b c)}^{a} = b^{a} c^{a}$
  - and into a sum?: $(A \to B + C) ≃ ?$

Every statement here is real mathematics. The one at the edge is the next question.

Our ambition

Collect every result of mathematics with simple and consistent notation.

We do not know yet whether this is possible. We are building Synthetic to find out.

Open Synthetic