Computer Supported Formal Work: Towards a Digital Mathematical Assistant
Serge Autexier · 2007
The year 2004 marked fiftieth birthday of first computer generated proof of a mathematical theorem: the sum of two even numbers is again an even number (with Martin Davis' implementation of Presburger Arithmetic in 1954). While Martin Davis and later research community of automated deduction used machine oriented calculi to find proof for a theorem by automatic means, Automath project of N.G. de Bruijn 1 - more modest in its aims with respect to automation - showed in late 1960s and early 70s that a complete mathematical textbook could be coded and proof-checked by a computer. Roughly at same time in 1973, Mizar project 2 started as an attempt to reconstruct mathematics based on computers. Since 1989, most important activity in Mizar project has been development of a database for mathematics. International cooperation resulted in creating a database which includes more than 7000 definitions of mathematical concepts and more than 42000 theorems. The work by Milner and others on LCF (28) spawned a research community on tactical theorem proving, which again modest with respect to automa- tion, showed that nevertheless important sequences of deduction could be encapsulated into a tactic and then invoked by mathematically trained user. Classical automated theorem proving procedures of today are based on ingenious search techniques to find a proof for a given theorem in very large search spaces - often in range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems auto- matically, their use in everyday mathematical practice is still limited. The shift from search based methods to more abstract planning techniques how- ever opened up a new paradigm for mathematical reasoning on a computer and several systems of new kind now employ a mix of interactive tactic based, search based as well as proof planning based techniques. The mega system is at core of several related and well-integrated research projects of mega research group, whose aim is to develop system support for working mathematician and formal software engineer, in particular it supports proof development at a human oriented level of abstraction. Sum-