Synthetic Mathematics in the Amazon

Talking about Synthetic Mathematics in the middle of the Amazon rainforest felt slightly surreal.

Parintins is famous for the Festival do Boi-Bumbá, for the river, for the forest, for the extraordinary cultural life of the Amazon. It is not the place most people imagine when they think about categorical logic, proof theory, Curry–Howard, or the future of AI-assisted mathematics.

And yet perhaps it was exactly the right place.

My talk at EMALCA Amazonas 2026 was about revolutions in mathematics: how mathematics periodically changes not only its results, but its understanding of what mathematics itself is.

The first great revolution of the twentieth century was the revolution of rigor. Frege, Hilbert, Gentzen, Gödel, Turing, Church: suddenly proofs themselves became mathematical objects. Formalization ceased to be merely philosophical and became technical infrastructure. Mathematics acquired syntax.

That revolution produced modern logic, proof theory, computability theory, formal systems, and eventually computer science itself.

But a second revolution was quietly unfolding in parallel.

The Curry–Howard correspondence — “proofs as programs, propositions as types” — revealed that proofs were not merely static certificates of truth. They had computational content. They could be transformed, executed, normalized, composed. Category theory then provided the missing global language of structure: proofs became morphisms, composition became central, and semantics became unavoidable.

I increasingly think that this second revolution is still incomplete.

We have the theory. We have fragments of the practice. But mathematics as a whole still has not fully absorbed the structural viewpoint introduced by categorical logic and semantics. Neither have Computer Science or Logic done the same. Why?

But now AI arrives.

Large language models can generate mathematical text at astonishing scale. They conjecture, sketch proofs, suggest strategies, translate between formalisms, and increasingly interact with proof assistants. Systems like Lean, Rocq, Isabelle, and Agda are no longer niche curiosities. Formal verification is becoming practical infrastructure.

And AI also reopens the oldest foundational wounds.

LLMs operate probabilistically, not semantically. They produce convincing mathematical language without any guarantees of correctness. They manipulate symbols fluently while remaining disconnected from proof in the classical sense.

This is why the current moment feels less like a purely technological revolution and more like the collision of earlier mathematical revolutions.

The first revolution demanded rigor. The second revealed deep structures connecting proofs, programs, and categories. The third — the AI revolution — suddenly makes those abstract structural questions operationally necessary.

What counts as a proof?
How do we represent mathematical structure?
How do we verify transformations?
What is the semantic content of a generated argument?
How do we move between informal mathematical language and formal systems?

These questions are no longer philosophical luxuries. They are engineering problems for the future of mathematics.

This is one reason I spoke about Dialectica categories in Parintins.

Gödel’s Dialectica interpretation and Girard’s linear logic both force us to think carefully about structure, interaction, resources, witnesses, and transformations. Category theory provides a language capable of relating these ideas without collapsing their distinctions.

I am not claiming that category theory “solves AI”.

Far from it. But I am claiming that the automation of mathematics makes it impossible to ignore semantics any longer.

For decades, categorical logic often seemed abstract, beautiful, and somewhat distant from mainstream mathematical practice. Today the situation is changing. As mathematical reasoning becomes partially automated, questions about meaning, translation, compositionality, verification, and structure move from the foundations to the center.

And perhaps this is why speaking about these ideas in the Amazon felt unexpectedly appropriate.

The Amazon constantly reminds us that scale changes everything. Small local interactions produce vast global structures. Networks matter. Flows matter. Translation between levels matters. Structure matters.

Mathematics is entering a similar moment. We are moving from isolated proofs to ecosystems of formalization, machine assistance, semantic translation, and large-scale mathematical computation. The foundational questions of the twentieth century are returning — but now under computational pressure.

The second revolution is no longer optional.