Formal Mathematics for Mathematicians Foreward to the Special Issue

Andrzej Trybulec Artur Kornilowicz Adam Naumowicz.

Krystyna Kuperberg

Received: 9October 2012/ Accepted: 10 October 2012/ Published online: 1 November 2012

O The Autbor(s) 2012. This article is publisbed with open access at Springerlink.com

Abstract The collection of works for this special issue was inspired by the pre-

sentations given at the 2011 AMS Special Session on Formal Mathematics for

Mathematicians: Developing Large Repositories of Advanced Mathematics. The issue

features a collection of articles by practitioners of formalizing proofs who share a

deep interest in making computerized mathematics widely available.

Keywords Formalization Repositories of mathematics

Mathematical proof reconstruction

1 Introduction

It has been shown in recent years that proof checkers and theorem provers can be

successfully used by mathematicians for automated proving and formal verification

of non-trivial results. One key to this success was the development of formalisms

close to the so-called "mathematical vernacular" in a way acceptable by mathe

maticians and software capable of processing such input. Numerous attempts have

been made to make the mathematical community more interested in all these

developments, to name just the four excellent papers that appeared in Notices of

A. Trybulee A. Kornilowicz A. Naumowicz (

Department of Mathematics and Informatics, University of Bialystok, Bialystok, Poland

e-mail: adamn@math.uwb.edu.pl

A. Trybulec

e-mail: trybulec@math.uwb.edu.pl

A. Kornilowicz

e-mail: arturk@math.uwb.edu.pl

K. Kuperberg

Department of Mathematics and Statistics, Auburn University, Auburn, AL, USA

e-mail: kuperkm@auburn.edu