[FOM] deautomatization in mathematics

[Saburou Saitoh]

Dear  foundations:

In the paper: [1] Paulson LC. Formalising Mathematics In Simple Type
Theory. arXiv preprint arXiv:1804.07860. 2018 Apr 20.
https://arxiv.org/abs/1804.07860
Professor Paulson stated:


The importance of legibility can hardly be overstated. A legible proof is
more
likely to convince a sceptical mathematician: somebody who doesn’t trust a
complex
software system, especially if it says x=0 = 0. While much research has gone
into the verification of proof procedures [32, 47], all such work requires
trusting
similar software. But a mathematician may believe a specific formal proof
if it can
be inspected directly, breaking this vicious cycle. Ideally, the
mathematician would
then gain the confidence to construct new formal proofs, possibly reusing
parts of
other proofs. Legibility is crucial for this.

On the fundamental result on x/0=0, please look the simple draft:

*viXra:1908.0100 <http://vixra.org/abs/1908.0100>* *submitted on 2019-08-06
20:03:01*, (789 unique-IP downloads)
Fundamental of Mathematics; Division by Zero Calculus and a New Axiom

With best regards,
Sincerely yours,

Saburou Saitoh
2019.10.8.18:42


2019年10月8日(火) 14:06 José Manuel Rodríguez Caballero <josephcmac at gmail.com>:

> 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/8bf475c5/attachment-0001.html>