[FOM] Errors discovered as a result of formalization

[José Manuel Rodriguez Caballero]

Tim wrote:
> On the other hand, I am interested in what obstacles are preventing proof
> assistants from becoming as widely adopted as, say, computer algebra
> systems or even LaTeX.


I will answer from my personal experience, which may not be the more typical situation.

Most times when I talk with a professional mathematician of an older generation about using proof-assistants in order to do research, the answer is: you should write the proof in paper first and then, formalize it in the proof assistant, but this last activity can be done by another person, so you can focus on the creative part of the work. It is the same attitude of a physicist towards mathematicians (there may be exceptions): the physicist do the creative work in physics and the mathematicians could formalize the physicist’s (informal) theories, e.g., Dirac delta function.

I do not share this point of view. I think that proof assistants may be useful for research because they detect subtle errors. For example, in the library (Isabelle/HOL) about functional analysis in which I am working, at the begging it was assumed that the pointwise sum of two closed subspaces of a Hilbert space was a closed subspace. Indeed, this result is true for finite dimensions, but Isabelle detected the error for infinite dimension. So, I easily corrected the library, by adding the topological closure to the sum,
as it can be seen from my GitHub history. The motivation behind this construction is quantum logic.

Are there researchers formalizing their own results in Isabelle/HOL, with publications about it? The answer is yes, here is an example:

Unruh, Dominique. "Quantum relational hoare logic." Proceedings of the ACM on Programming Languages3.POPL (2019): 33

https://arxiv.org/pdf/1802.03188.pdf

Kind Regards,
José M.


Sent from my iPhone
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200116/65b44c70/attachment-0001.html>