[FOM] f.o.m. documentary 2

[Andrej Bauer]

> 3. Focus on developing interactions between mathematical logic and areas of
> core mathematics.

The given account lacks some important examples of the above point:

1. Developments in categorical logic reveal important and deep
interaction between logic and category theory (or algebra, if you
will), especially sheaf theory and topos theory. For example, they
elucidate the relationship between Cohen forcing and Grothendieck's
constructions which originated from algebraic geometry, if I am not
mistaken, certainly an amazing connection.

2. Recent developments in type theory reveal important and deep
intereaction between type theory and homotopy theory. It is perhaps
too early to pass a definitive judgment, but the connections certainly
look promising.

A well balanced documentary would presumably not omit these points.

Another thing worth mentioning somewhere is the steady progress that
is being made in computerization of mathematics. Just the potential
for computers to become competent assistants to professional
mathematicians is worth a notice, as this would greatly change how we
do mathematics.

With kind regards,

Andrej