The gradual computerisation of mathematics in MathLang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The MathLang project aims at computerizing mathematical texts according to various degrees of formalisations, and without any prior commitment to a particular logical framework (e.g., having to choose either set theory or category theory or type theory, etc.) or to a particular proof checker (e.g., having to choose Mizar or Isabelle or Coq, etc.). Instead, MathLang keeps the choices of the logical framework and proof checker open depending on the taste and expertise of the user. Furthermore, MathLang allows useful computerizations of mathematical texts at much lower levels where the emphasis is not on full formalization as is done in the foundations of mathematics (e.g., as initiated by Frege and Russell) or on proof checking (e.g., as initiated by de Bruijn's Automath). During computerization, first, the mathematical text is input into the computer exactly as it was written and then one or more MathLang aspects are applied to the text to provide extended versions of the text that can be checked for different levels of correctness. One basic aspect is to extend the text with categorical information (term, noun, adjective, statement, etc) and to automatically check the correctness of the text at this categorical level. This guarantees coherence of the text (e.g., variables are declared before being used and the text constitutes a well structured book). Another aspect is to divide the text into parts annotated with relations (e.g., Corollary A uses Theorem B) and to automatically derive from these relations a number of structures that represent some dependencies in the text which help explain the logical structure of the text. These dependencies are used in a further aspect where a version of the text is transformed into another which shows the holes in the proofs. Other aspects will transform this version into a fully formalized version (say in Mizar or Isabelle). MathLang was created in 2000 by Fairouz Kamareddine and J.B. Wells as an experience driven project where the computerisation of different texts taken from various branches of mathematics, is the basis for the design and implementation of the MathLang aspects. So far, a number of mathematical texts have been computerised, some of which have been gradually transformed through MathLang aspects into full Mizar. Other proof checkers (e.g., Isabelle and Coq) are envisioned for the near future. In this talk, the MathLang framework, its developments and its current and future aspects, as well as examples of computerization from original mathematical texts to the fully formalised Mizar versions are given. For each aspect, emphasis will be on its design, formalisation, implementation, the automation available for this aspect and the correctness or trustworthiness of these processes. Then, we discuss how the computerisation path from the original mathematical text to full Mizar will look if Isabelle was the checker chosen instead of Mizar and show that a number of aspects and computerised versions of the original text are common between both path. We also discuss at which stage a commitment to a certain logical framework and a certain proof checker can be made on the path from the original mathematical text to the version fully formalised in that proof checker. The MathLang project started in 2000 by Fairouz Kamareddine and Joe Wells and has had since 2002 three PhD students (Manuel Maarek, Krzysztof Retel and Robert Lamar) and a number of MSc and BSc students all collaborating and contributing to the design and implementation of the various aspects and to the computerization of mathematical texts. © 2008 IEEE.

Original languageEnglish
Title of host publicationProceedings - 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007
Pages3-
DOIs
Publication statusPublished - 2007
Event9th International Symposium on Symbolic and Numeric lgorithms for Scientific Computing - Timisoara, Romania
Duration: 26 Sep 200729 Sep 2007

Conference

Conference9th International Symposium on Symbolic and Numeric lgorithms for Scientific Computing
Abbreviated titleSYNASC 2007
CountryRomania
CityTimisoara
Period26/09/0729/09/07

Fingerprint

Computerization
Mathematics
Logic
Isabelle
Formalization
Correctness
Categorical
Corollary
Automation
Theory Theory
Foundations of Mathematics
Expertise
Hole
Set Theory
Trustworthiness
Category Theory
Adjective
Nouns
Gottlob Frege

Cite this

Kamareddine, F. (2007). The gradual computerisation of mathematics in MathLang. In Proceedings - 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007 (pp. 3-) https://doi.org/10.1109/SYNASC.2007.85
Kamareddine, Fairouz. / The gradual computerisation of mathematics in MathLang. Proceedings - 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007. 2007. pp. 3-
@inproceedings{6d5f7f28c9d043ec951e06cfe4e0b54d,
title = "The gradual computerisation of mathematics in MathLang",
abstract = "The MathLang project aims at computerizing mathematical texts according to various degrees of formalisations, and without any prior commitment to a particular logical framework (e.g., having to choose either set theory or category theory or type theory, etc.) or to a particular proof checker (e.g., having to choose Mizar or Isabelle or Coq, etc.). Instead, MathLang keeps the choices of the logical framework and proof checker open depending on the taste and expertise of the user. Furthermore, MathLang allows useful computerizations of mathematical texts at much lower levels where the emphasis is not on full formalization as is done in the foundations of mathematics (e.g., as initiated by Frege and Russell) or on proof checking (e.g., as initiated by de Bruijn's Automath). During computerization, first, the mathematical text is input into the computer exactly as it was written and then one or more MathLang aspects are applied to the text to provide extended versions of the text that can be checked for different levels of correctness. One basic aspect is to extend the text with categorical information (term, noun, adjective, statement, etc) and to automatically check the correctness of the text at this categorical level. This guarantees coherence of the text (e.g., variables are declared before being used and the text constitutes a well structured book). Another aspect is to divide the text into parts annotated with relations (e.g., Corollary A uses Theorem B) and to automatically derive from these relations a number of structures that represent some dependencies in the text which help explain the logical structure of the text. These dependencies are used in a further aspect where a version of the text is transformed into another which shows the holes in the proofs. Other aspects will transform this version into a fully formalized version (say in Mizar or Isabelle). MathLang was created in 2000 by Fairouz Kamareddine and J.B. Wells as an experience driven project where the computerisation of different texts taken from various branches of mathematics, is the basis for the design and implementation of the MathLang aspects. So far, a number of mathematical texts have been computerised, some of which have been gradually transformed through MathLang aspects into full Mizar. Other proof checkers (e.g., Isabelle and Coq) are envisioned for the near future. In this talk, the MathLang framework, its developments and its current and future aspects, as well as examples of computerization from original mathematical texts to the fully formalised Mizar versions are given. For each aspect, emphasis will be on its design, formalisation, implementation, the automation available for this aspect and the correctness or trustworthiness of these processes. Then, we discuss how the computerisation path from the original mathematical text to full Mizar will look if Isabelle was the checker chosen instead of Mizar and show that a number of aspects and computerised versions of the original text are common between both path. We also discuss at which stage a commitment to a certain logical framework and a certain proof checker can be made on the path from the original mathematical text to the version fully formalised in that proof checker. The MathLang project started in 2000 by Fairouz Kamareddine and Joe Wells and has had since 2002 three PhD students (Manuel Maarek, Krzysztof Retel and Robert Lamar) and a number of MSc and BSc students all collaborating and contributing to the design and implementation of the various aspects and to the computerization of mathematical texts. {\circledC} 2008 IEEE.",
author = "Fairouz Kamareddine",
year = "2007",
doi = "10.1109/SYNASC.2007.85",
language = "English",
isbn = "0769530788",
pages = "3--",
booktitle = "Proceedings - 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007",

}

Kamareddine, F 2007, The gradual computerisation of mathematics in MathLang. in Proceedings - 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007. pp. 3-, 9th International Symposium on Symbolic and Numeric lgorithms for Scientific Computing, Timisoara, Romania, 26/09/07. https://doi.org/10.1109/SYNASC.2007.85

The gradual computerisation of mathematics in MathLang. / Kamareddine, Fairouz.

Proceedings - 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007. 2007. p. 3-.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - The gradual computerisation of mathematics in MathLang

AU - Kamareddine, Fairouz

PY - 2007

Y1 - 2007

N2 - The MathLang project aims at computerizing mathematical texts according to various degrees of formalisations, and without any prior commitment to a particular logical framework (e.g., having to choose either set theory or category theory or type theory, etc.) or to a particular proof checker (e.g., having to choose Mizar or Isabelle or Coq, etc.). Instead, MathLang keeps the choices of the logical framework and proof checker open depending on the taste and expertise of the user. Furthermore, MathLang allows useful computerizations of mathematical texts at much lower levels where the emphasis is not on full formalization as is done in the foundations of mathematics (e.g., as initiated by Frege and Russell) or on proof checking (e.g., as initiated by de Bruijn's Automath). During computerization, first, the mathematical text is input into the computer exactly as it was written and then one or more MathLang aspects are applied to the text to provide extended versions of the text that can be checked for different levels of correctness. One basic aspect is to extend the text with categorical information (term, noun, adjective, statement, etc) and to automatically check the correctness of the text at this categorical level. This guarantees coherence of the text (e.g., variables are declared before being used and the text constitutes a well structured book). Another aspect is to divide the text into parts annotated with relations (e.g., Corollary A uses Theorem B) and to automatically derive from these relations a number of structures that represent some dependencies in the text which help explain the logical structure of the text. These dependencies are used in a further aspect where a version of the text is transformed into another which shows the holes in the proofs. Other aspects will transform this version into a fully formalized version (say in Mizar or Isabelle). MathLang was created in 2000 by Fairouz Kamareddine and J.B. Wells as an experience driven project where the computerisation of different texts taken from various branches of mathematics, is the basis for the design and implementation of the MathLang aspects. So far, a number of mathematical texts have been computerised, some of which have been gradually transformed through MathLang aspects into full Mizar. Other proof checkers (e.g., Isabelle and Coq) are envisioned for the near future. In this talk, the MathLang framework, its developments and its current and future aspects, as well as examples of computerization from original mathematical texts to the fully formalised Mizar versions are given. For each aspect, emphasis will be on its design, formalisation, implementation, the automation available for this aspect and the correctness or trustworthiness of these processes. Then, we discuss how the computerisation path from the original mathematical text to full Mizar will look if Isabelle was the checker chosen instead of Mizar and show that a number of aspects and computerised versions of the original text are common between both path. We also discuss at which stage a commitment to a certain logical framework and a certain proof checker can be made on the path from the original mathematical text to the version fully formalised in that proof checker. The MathLang project started in 2000 by Fairouz Kamareddine and Joe Wells and has had since 2002 three PhD students (Manuel Maarek, Krzysztof Retel and Robert Lamar) and a number of MSc and BSc students all collaborating and contributing to the design and implementation of the various aspects and to the computerization of mathematical texts. © 2008 IEEE.

AB - The MathLang project aims at computerizing mathematical texts according to various degrees of formalisations, and without any prior commitment to a particular logical framework (e.g., having to choose either set theory or category theory or type theory, etc.) or to a particular proof checker (e.g., having to choose Mizar or Isabelle or Coq, etc.). Instead, MathLang keeps the choices of the logical framework and proof checker open depending on the taste and expertise of the user. Furthermore, MathLang allows useful computerizations of mathematical texts at much lower levels where the emphasis is not on full formalization as is done in the foundations of mathematics (e.g., as initiated by Frege and Russell) or on proof checking (e.g., as initiated by de Bruijn's Automath). During computerization, first, the mathematical text is input into the computer exactly as it was written and then one or more MathLang aspects are applied to the text to provide extended versions of the text that can be checked for different levels of correctness. One basic aspect is to extend the text with categorical information (term, noun, adjective, statement, etc) and to automatically check the correctness of the text at this categorical level. This guarantees coherence of the text (e.g., variables are declared before being used and the text constitutes a well structured book). Another aspect is to divide the text into parts annotated with relations (e.g., Corollary A uses Theorem B) and to automatically derive from these relations a number of structures that represent some dependencies in the text which help explain the logical structure of the text. These dependencies are used in a further aspect where a version of the text is transformed into another which shows the holes in the proofs. Other aspects will transform this version into a fully formalized version (say in Mizar or Isabelle). MathLang was created in 2000 by Fairouz Kamareddine and J.B. Wells as an experience driven project where the computerisation of different texts taken from various branches of mathematics, is the basis for the design and implementation of the MathLang aspects. So far, a number of mathematical texts have been computerised, some of which have been gradually transformed through MathLang aspects into full Mizar. Other proof checkers (e.g., Isabelle and Coq) are envisioned for the near future. In this talk, the MathLang framework, its developments and its current and future aspects, as well as examples of computerization from original mathematical texts to the fully formalised Mizar versions are given. For each aspect, emphasis will be on its design, formalisation, implementation, the automation available for this aspect and the correctness or trustworthiness of these processes. Then, we discuss how the computerisation path from the original mathematical text to full Mizar will look if Isabelle was the checker chosen instead of Mizar and show that a number of aspects and computerised versions of the original text are common between both path. We also discuss at which stage a commitment to a certain logical framework and a certain proof checker can be made on the path from the original mathematical text to the version fully formalised in that proof checker. The MathLang project started in 2000 by Fairouz Kamareddine and Joe Wells and has had since 2002 three PhD students (Manuel Maarek, Krzysztof Retel and Robert Lamar) and a number of MSc and BSc students all collaborating and contributing to the design and implementation of the various aspects and to the computerization of mathematical texts. © 2008 IEEE.

UR - http://www.scopus.com/inward/record.url?scp=48049122874&partnerID=8YFLogxK

U2 - 10.1109/SYNASC.2007.85

DO - 10.1109/SYNASC.2007.85

M3 - Conference contribution

SN - 0769530788

SN - 9780769530789

SP - 3-

BT - Proceedings - 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007

ER -

Kamareddine F. The gradual computerisation of mathematics in MathLang. In Proceedings - 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007. 2007. p. 3- https://doi.org/10.1109/SYNASC.2007.85