View: session overviewtalk overview

13:00 | How Natural is Formal Mathematics? PRESENTER: Michael Junk ABSTRACT. We present results from a lecture on mathematical modeling where both lectures and homework assignments are based on an editor which checks a formal syntax and the correct use of names. Since the lecture addresses students without prior training or special inclination to for- mal mathematics our observations shed some light on the ambivalent relation between formality and naturalness. |

13:30 | (Invited talk) Formal Proofs for the Future ABSTRACT. . |

15:00 | (Invited talk) The evolution of the language of mathematics |

16:30 | Formalizing Foundational Notions in Naproche-SAD (4 short talks) PRESENTER: Peter Koepke ABSTRACT. We present three current formalization projects with the proof assistant Naproche-SAD. Naproche-SAD formalizations use the natural mathematical input language ForTheL and in favorable cases read like textbook material. In this paper we emphasize the encoding of basic notions and axioms on the basis of inbuilt or slightly modified mechanisms of Naproche-SAD. The formalizations concern an introduction into set theory up to substantial results in infinitary combinatorics, a general theory of structures which are all made pairwise disjoint to avoid ambiguities, and an introduction to abstract linear algebra where for ef- ficiency reasons the type system is restricted to a single type "object", which is hard-coded into Naproche-SAD. |

17:30 | Integrating Formal Methods into LaTeX Workflows PRESENTER: Dennis Müller ABSTRACT. While some mathematicians have begun actively adapting formal methods for their work, there is a prohibitively large discrepancy between the way new mathematical results are developed, presented and published in mathematical practice, and the way they are formalized and implemented in formal systems. This discrepancy is primarily due to the respective surface languages and the logical foundations used in theorem prover systems. The former tend to be more reminiscent of programming languages with strict formal grammars than (informal) mathematical language, whereas the latter are most prominently variants of type theories – both of which require considerable effort to learn and understand for users unfamiliar with them. Consequently, many mathematicians complain that • formal systems are difficult to learn and use, even if one is well acquainted with the (informal) mathematics involved, • they require a level of detail in proofs that is prohibitive even for “obvious” conclusions, • their libraries are difficult to grasp without already being familiar with the system’s language, conventions and functionalities. Consequently, the utility of formalizing mathematical results can be too easily (and too often is) dismissed in light of the additional time and work required even for experts. This is despite the fact that many services available for formal mathematics are already enabled by semi-formal (or flexiformal) representations, such as semantic annotations in natural language texts, or formal representations containing opaque informal expressions. Therefore, we need to invest into methods for bridging the gap between informal mathematical practice and (semi-)formal mathematics. However, the vast majority of mathematicians can safely be assumed to be comfortable with using LaTeX and do so on a regular basis. The second author developed the STeX package for LaTeX, specifically for annotating mathematica documents with structural and formal semantics. In particular, STeX is based on an OMDoc ontology, which is foundation-agnostic in the sense that it does not favor a specific foundation (such as type or set theories) over any other. This approach is consequently best suited for semantifying informal documents, where foundations are often unspecified, left implicit or switched fluently. Furthermore, STeX allows markup both on the level of mathematical expressions as well as on a structural level, such as declarations, definienda/definientia and theorems. The SMGloM library [Koh14] (Semantic Multilingual Glossary of Mathematics) contains hundreds of STeX-annotated concepts and definitions, providing LaTeX-macros for their symbolic notations (i.e. presentation as pure LaTeX) in signature files. These are documented in various natural language dictionary entries, defining and describing the concepts in a flexiformal manner. Besides natural languages, the SMGloM could conceivably be extended to cover controlled languages such as Naproche, or fully formal languages such as those associated with interactive theorem provers. In addition to being valid LaTeX compilable via pdflatex, STeX-documents can be transformed to OMDoc using the LaTeXML-software [Gin+11], yielding a formally disambiguated representation of the document and in particular the symbolic expressions therein. STeX itself is integrated, and shares an underlying OMDoc ontology, with the MMT system – a foundation-independent meta-framework and API for knowledge management services. This integration makes the generic services provided by MMT – e.g. type checking, library management/browsing, translation – available to informal mathematical texts. Using alignments, OMDoc-expressions can be translated between different libraries, languages and foundations. This allows for e.g. translating (originally) STeX-content to a typed setting in order to e.g. check expressions and run type inference. Additionally, several theorem prover libraries have been translated to OMDoc and integrated in the MMT system. Extending these integrations to enable exporting from MMT as well (and in conjunction with natural language processing), this could enable verifying informal mathematics imported via STeX using external state-of-the-art theorem prover systems. We propose to 1. extend the STeX package to be compatible with arbitrary LaTeX document classes and packages, as well as dedicated macros covering a multitude of common styles of presentation and linguistic phenomena in scientific documents 2. aligning the (ever growing) SMGloM concepts with their counterparts in formal languages, so that the SMGLoM can serve as a true Math-in-the-Middle library for translation between languages, 3. develop an IDE that specifically supports and suggests STeX macros to significantly lower the entry barrier and allows accessing MMT's formal services directly, and 4. extend MMT by new helpful services for STeX content. |

18:00 | Why We Need Structured Proofs in Mathematics PRESENTER: Mauricio Ayala-Rincón ABSTRACT. When mathematicians write a standard proof of some theorem, they have to decide on which level of detail they will present their argument. If they provide too little justification, readers may spend a lot of time filling the holes left or, even worse, may not understand why a specific step of the proof is (or not) correct. However, more argumentation is not necessarily always better, since this may obscure the "big picture" and some readers may be more interested in seeing the "big picture" than in checking every tiny detail of the proof. Therefore, the ideal level of detail in a mathematical proof varies from reader to reader, as it depends on the reader's previous knowledge and the reader’s intention. The standard way of writing mathematical proofs, which will henceforth be called prose proofs, cannot satisfy everyone. In contrast with prose proofs, we have the concept of structured proofs. In a structured proof, the steps and substeps are hierarchically presented. The proof is decomposed as a tree of steps, and each step can be further decomposed into smaller subtrees of substeps and so on. By correctly numerating each step and by using the right indentation, the hierarchy of the proof is clear at first sight. Examples of structured proofs can be found in the extended version of this paper, available at http://ayala.mat.unb.br/publications.html. If writing structured proofs is accompanied by the discipline of explaining every step in meticulous detail, the probability of obtaining an incorrect proof or a wrong result diminishes. That is because the hierarchy of the proof will allow the writer to add justifications to a given step without "clouding" other steps of the proof, and also make it easier to check if all the corner cases were handled. Since structured proofs can make it harder to obtain an incorrect result, a comparison may arise between structured proofs and interactive theorem provers (ITPs). By using an ITP, the chances of obtaining an incorrect result are significantly lower than by using a structured proof, as the computer checks every step of the proof. However, structured proofs also have advantages over ITPs, as they are faster to write and more readable. As members of a research group bridging interest from graduate programs in Mathematics and Computer Science we also have a huge interest in motivating mathematicians to use ITPs. For this we have developed mathematical theories in PVS as well as short-courses to attract the interest of such audience. |