The most powerful language for mathematics according to M. Gromov

[José Manuel Rodríguez Caballero]

Dear FOM members,
  I would like to share the following quotations from M. Gromov concerning
the most powerful language for mathematics according to him. In his paper
on entropy, M. Gromov wrote (page 2 of [1]) :

Arguably, the category language, some call it abstract, reflects mental
> undercurrents that surface as our intuitive reasoning; a comprehensive
> mathematical description of this reasoning, will be, probably, even further
> removed from the real world than categories and functors.


In his second lecture about his paper [1], M. Gromov (min 21 of [2])
continues his defense of the language of categories:

If you cannot say something in categorical language, possibly go to the
> higher level, but more likely you are just stupid enough that you do not
> know how to say it. And people hate categories, because they do not know
> how to say [...] Categories is the most primitive language available to us
> and therefore the most powerful.


It would be interesting to know whether or not there are mathematicians in
this list who disagree with this point of view and which language they
would like to propose as the most powerful for mathematics?

In my opinion, the language of simple type theory is enough for the sort of
mathematics that I encounter in my personal research (quantum cryptography,
elementary number theory, context-free grammar) and it is the most powerful
for me because of automation in proof assistants. Nevertheless,
mathematicians working in other areas of mathematics may have their own
preferred languages, e.g., for Voevodsky [4], following Grothendieck [3],
it was homotopy type theory rather than category theory his preferred
language (homotopy type theory can be developed independently of category
theory [5]).

Kind regards,
Jose M.

References:
[1] Gromov, M., 2013. In a search for a structure, part 1: On entropy.
Entropy, 17, pp.1273-1277.
URL =
https://pdfs.semanticscholar.org/3137/66d8f87b29eeae9004d8c1eb5f8a8fb26cf3.pdf

[2] Lecture: Mikhael Gromov - 2/6 Probability, symmetry, linearity
URL = https://youtu.be/Vci3C6yAzRE?t=1307
<https://youtu.be/Vci3C6yAzRE?t=1279>

[3] Grothendieck, A., 1997. Esquisse d'un programme. London Mathematical
Society Lecture Note Series, pp.5-48.

[4] Voevodsky, V., 2011, May. Univalent foundations of mathematics. In
International Workshop on Logic, Language, Information, and Computation
(pp. 4-4). Springer, Berlin, Heidelberg.

[5] Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M. and
Spitters, B., 2017, January. The HoTT library: a formalization of homotopy
type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on
Certified Programs and Proofs (pp. 164-172).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200203/d8bbd645/attachment.html>