[FOM] deautomatization in mathematics

[José Manuel Rodríguez Caballero]

Dear FOM members,
  I would like to begin with a quotation from [1]:

Proof assistants must be capable of performing lengthy deductions
> automatically. But more expressive formalisms are more difficult to
> automate. Even
> at the most basic level, technical features of constructive type theories
> interfere with
> automation.


This principle may suggest a one-dimensional polarization in the
formalization of mathematics as follows: on one extreme we may have the
most expressive formalization of mathematics and on the other extreme we
may have the formalization of mathematics which is better for automation. I
would like to distinguish two processes:

- mathematical automatization: A translation of a theory from a formalism
to another one which is more efficient for automation, but less expressive.

- mathematical deautomatization: A translation of a theory from a formalism
to another one which is more expressive, but less efficient for automation.

On the one hand, mathematical automation is useful in order to reduce some
of the tasks (not all) of a mathematician to a microprocessor. On the other
hand, the importance of mathematical deautomatization is more mysterious.
So, I would like to ask for examples of deautomatization in the history of
mathematics, i.e., the renunciation of efficient automation in order to
obtain more expressive power.

Sincerely yours,
José M.

References:
[1] Paulson LC. Formalising Mathematics In Simple Type Theory. arXiv
preprint arXiv:1804.07860. 2018 Apr 20. https://arxiv.org/abs/1804.07860
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20191008/98597b93/attachment.html>