### Abstract

In this paper we are interested in the process of formalizing a mathematical text written in Common Mathematical Language (CML) into type theory using intermediate representations in Weak Type Theory [8] and in type theory with open terms. We demonstrate that this method can be reliable not only in the sense that eventually we get formally verified mathematical texts, but also in the sense that we can have a fairly high confidence that we have produced a ‘faithful’ formalization (i.e. that the formal text is as close as possible to the intentions expressed in the informal text).
A computer program that assists a human along the formalization path should create enough "added value" to be useful in practice. We also discuss some problems that such an implementation needs to solve and possible solutions for them.

Original language | English |
---|---|

Title of host publication | Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004) |

Editors | A. Asperti, G. Bancerek, A. Trybulec |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 145-159 |

ISBN (Print) | 3-540-23029-7 |

DOIs | |

Publication status | Published - 2004 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Volume | 3119 |

ISSN (Print) | 0302-9743 |

## Fingerprint Dive into the research topics of 'A path to faithful formalizations of mathematics'. Together they form a unique fingerprint.

## Cite this

Jojgov, G. I., & Nederpelt, R. P. (2004). A path to faithful formalizations of mathematics. In A. Asperti, G. Bancerek, & A. Trybulec (Eds.),

*Mathematical Knowledge Management (Proceedings Third International Conference, MKM2004, Bialowieza, Poland, September 19-21, 2004)*(pp. 145-159). (Lecture Notes in Computer Science; Vol. 3119). Berlin: Springer. https://doi.org/10.1007/978-3-540-27818-4_11