Question

When the paper The unification of Mathematics via Topos Theory by Olivia Caramello, says "one can generate a huge number of new results in any mathematical field without any creative effort." is this an exaggeration, and if not is this a new idea or has it always been thought that topos theory could enable automatic generation of theorems.

Answer 1

This statement is true, but there's substantially less than meets the eye to it.

Topoi are gadgets which are both models of both a fairly large fragment of logic (typed higher-order logic), and are generalizations of sheaves on a topological space. (The reason this connection is possible is morally that the open sets of a topological space form a Heyting algebra, which is a model of propositional intuitionistic logic.) As a result of their high logical strength, you can take many practical constructions and encode them in the internal logic of a topos. Then you can take an external view and hit these constructions with topologist technical wizardry.

Since topologists and logicians talk to each other rather less frequently than we ought to, this method is a very fertile source of theorems. "Without creative effort" is just a rhetorical flourish intended to encourage people to learn about topoi -- there's no way (presently) that a computer could generate theorems via topos theory. But it is an effective tool for human mathematicians to port ideas from one area to another, which has always been a productive endeavor.

The book to read on this subject is MacLane and Mordeijk's Sheaves in Geometry and Logic, which, as you can guess from the title, emphasizes the moral that taking a synthesizing perspective on mathematics is often valuable.

Answer 2

I can't really answer the question, but I attended Olivia's talk today at CT2010 in Genova where she was presenting this paper, and I asked her some questions afterwards. Any errors or misrepresentations in my following comments are entirely mine.

When the informal statement is made technical, there appear to be some qualifications. First, it applies only to mathematical theories that can be formalized in geometric logic. This is a kind of logic with a restriction on how quantifiers can be used in axioms. According to Olivia, this is not much of a restriction, because it includes for example finitary logic, and more.

Second, to be able to transport results from one theory to another, the theories must be Morita equivalent. Apparently this is more common than one might think, and once one has Morita equivalence, one can transport all kinds of results back and forth. So perhaps it would be fair to say that "some creative effort" goes into finding appropriate Morita equivalences in the first place.

Olivia refered to her Ph.D. thesis for a number of examples where this had been done. I have not really seen the examples. The areas of mathematics that she specifically mentioned in her talk were algebra, topology, two different branches of logic (proof theory and model theory), and a 5th one which I forgot. Definitely not PDE's or Riemannian geometry.

Two more remarks: a topos is a kind of set theory, so it is indeed plausible that all kinds of areas of mathematics can be formalized within a topos. Sometimes this is done by "real" mathematicians (i.e., non-logicians). For example, Tom Hales's ongoing formalization of the proof of the Kepler conjecture is done in HOL Light, which uses a topos logic as far as I remember. (The proof is not constructive, as excluded middle and the axiom of choice have been added as additional axioms). Tom has already given a complete machine-checkable proof of the Jordan curve theorem. The point of doing this in HOL Light, at this point, is not so much the topos aspect, but the fact that the proofs can be verified by machine, eliminating the referee's residual uncertainty. This is impractical with "ordinary" set theory.

Last, when one claims to be able to generate "new theorems", this does not necessarily mean "interesting new theorems". I guess that in some cases, they can be interesting, but perhaps more so to logicians than to other mathematicians. Then again, it's happened before that disjoint areas of mathematics were related, and when this happens, it is always useful. Seems nice to have another avenue.

Answer 3

Topos theory provides a dictionary between (certain areas of) logic and (certain areas of) geometry. As such, it provides all the benefits that mathematical dictionaries do: It lets you translate between two languages whose natural evolutions proceeded independently. An insight that is obvious in one domain may not be so obvious when translated to the other domain.

Dictionaries cannot perform magic. In particular, it is usually too optimistic to think that a dictionary will allow you to prove significant new theorems with no effort. True, sometimes we do get lucky in this way. When Richard Stanley first discovered the dictionary between toric varieties and convex polytopes, he almost immediately reaped the reward of proving an important combinatorial conjecture with very little effort, because geometers had already put in a lot of work to solve exactly the problem he needed. But more commonly, the payoff of a dictionary is that it allows you to formulate good questions with very little effort. That is, you now have a new way to think about old problems, so you may be able to find your way more easily to a solution by borrowing concepts from both domains. You will still need to do hard work to solve hard problems, but your toolbox is now bigger.

Answer 4

When a phrase is taken from a context, it is easy to misread it. If one looks at the paper, "one can generate a huge number of new results in any mathematical field without any creative effort" makes sense and is justified.

The idea is that most Mathematics can be formalized as a geometric theory, i.e, a logical theory with infinitary disjunction and finitary conjunction with the natural rules of inference. This is true since most Mathematics can be formalized in first-order logic which can be translated in geometric logic, and the translation preserves set-theoretic models. The model theory of geometric logic is naturally categorical; in fact, it is sound and complete (in a strong sense) when one considers the categorical models living inside Grothendieck toposes. The completeness theorem is proved by constructing a universal model which lives in a special topos, the classifying topos.

Olivia's result shows that very different theories share the same classifying topos (or better, they have different but equivalent classifying toposes). When this fact happens, and it is not uncommon - Olivia provides very general techniques to achieve this result - the classifying topos allows to move results from one theory to another. Examples have shown that very simple results in one theory translate into very deep results in other theories. But the translation technique is not-dictionary oriented but rather "modulo an abstract invariant" which allows for an extremly high degree of freedom.

The interesting thing in this machinery, which is not automatic, is exactly that a huge number of new mathematical results in any field of Mathematics can be generated without any significant creative effort. Of course, not every result can be generated in this way, as far as we know now, and not every generated result is significant. The mathematical intuition of an educated mathematician is needed to choose the right theories and the correct invariant to achieve a significant result. Olivia's examples show that very simple invariants applied to very classical theories provide explanations to deep results and a couple of new interpretation of classical results have been obtained.

As far as I'm able to understand Olivia's results, I believe her conclusions because her articles prove them. Of course, my understanding is not perfect and the explanation above are approximations of the real results. And yes, she is doing a big claim - but I became convinced that it is a true one.

Answer 5

It would be presumptuous on my part to attempt to answer this question, but I want to share with other MOers this recent paper

http://www.ihes.fr/~lafforgue/math/TheorieCaramello.pdf

of Laurent Lafforgue and this video

https://sites.google.com/site/logiquecategorique/Contenus/20130227_Lafforgue

of one of his recent lectures, [dont] le but [] est de poser cette question (inspirée par la théorie de Caramello) : l'indépendance de $l$ de la cohomologie $l$-adique et la correspondance de Langlands sont-elles des équivalences de Morita entre topos classifiants ?

Here is a quote from the paper : La théorie de Caramello... offre déjà un très grand nombre d'exemples d'équivalences de Morita et de leurs applications. Ces exemples sont étonnament divers et ils apparaissent presque toujours comme surprenants. Beaucoup d'énoncés auraient été très difficiles à démontrer, et plus encore à imaginer, sans les topos et sans les méthodes de calcul que la théorie des topos classifiants et des équivalences de Morita rend possibles et naturelles. Quand on songe que la correspondance de Langlands ressemble beaucoup à une equivalence de Morita et qu'elle en est peut-être une, on se dit que le champ ouvert à cette théorie est immense.