[FOM] deautomatization in mathematics

[Josef Urban]

The proof of Robbins conjecture found by EQP has been de-automated,
human-explained, and human-formalized in PAs (e.g. Mizar).

Unfortunately, we don't have today good tools to automatically translate
very long proofs (10k-100k steps) found by e.g. Prover9 in quasigroup
theory into "structural", "human-understandable" proofs (typically
requiring at least HOL, set theory, etc.).

I'd also say that "automation" is moving to more expressive logics these
days. E.g. in our recent GRUNGE benchmark (https://arxiv.org/abs/1903.02539),
an ATP system (Leo-III) targeting the HOL logic directly has beaten the
systems that work only after translation to FOL. The same for systems that
do tactical search directly in the more expressive settings - e.g.
TacticToe (https://arxiv.org/abs/1804.00596).

Josef




On Tue, Oct 8, 2019 at 7:06 AM José Manuel Rodríguez Caballero <
josephcmac at gmail.com> wrote:

> 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
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20191008/b5fdb716/attachment-0001.html>