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 or to a particular proof checker. In this paper, 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.
