Workshop on Automated Mathematical Theory Exploration 2009




Research Institute for Symbolic Computation
Johannes Kepler University Linz


uni-edinburg  uni-edinburg2

Research Institute e-Austria Timisoara 
West University of Timisoara


June 29-30, 2009, Hagenberg, Austria


General Information

The first International workshop on Mathematical Theory Exploration (AUTOMATHEO'09) will take place in Hagenberg, Austria, at the Research Institute for Symbolic Computation (RISC), June 29-30, 2009.

Topics include all aspects of Mathematical Theory Exploration and their relations with other parts of mathematics, physics, computer science, and biology.

Program Committee

Bruno Buchberger, Roy McCasland and Adrian Craciun – General Chairmen

Tudor Jebelean

Wolfgang Windsteiger

Temur Kutsia

Florina Piroi

Nikolaj Popov

Alan Smaill

Lilia Georgieva

Lucas Dixon

Fiona McNeill


As a matter of fact, automated reasoning (automated theorem proving)- despite impressive advances in the reasoning technology - so far had very little influence on  the every-day work of mathematicians, whereas it had quite some impact on a few selected application areas like logic programming, hardware verification, and artificial intelligence. We believe that the reason for this is that main stream automated reasoning focused on


– the automated proof of isolated theorems (given a certain knowledge base, mostly axioms), see the typical examples in the CADE theorem proving competition


– and the usage of general reasoning methods (like the resolution method) uniformly for all areas of mathematics. In contrast, the practical reasoning activities of "working mathematicians" proceed


– by building up theories in structured layers (inventing definitions, inventing and proving lemmata and theorems, inventing problems, inventing and proving algorithms) so that in most of the incremental steps relatively easy proving is sufficient


– and by using many different special reasoning techniques for the various theories at hand.


We believe that this structured and theory-dependent approach to mathematical reasoning is the reason why, for human mathematicians, building up complicated mathematical theories is possible at all.


Therefore, in the talk "Theorem Proving Versus Theory Exploration" at the Calculemus Workshop in Trento 1999 and in the Workshop "Mathematical Knowledge Management (MKM)" which we organized, for the first time 2001 at RISC,  we advocated that, at least for the application of automated reasoning in mathematics, we should shift the attention to  the Automation of Mathematical Theory Exploration rather than considering only the proof of isolated theorems. In the meantime, quite some researchers have started to work in the area of Mathematical Knowledge Management (documented in the series of MKM conferences).


In this Workshop AUTOMATHEO (Automated Mathematical Theory Exploration) we gather for discussing approaches to one particularly challenging and not yet heavily studied aspect of automated theory exploration, namely the computer-supported invention of definitions, theorems, problems, and algorithms, which of course cannot be seen independent of proving.  We hope that from this first meeting of groups working in the area of automated invention in mathematics some impulse will be generated for more intensive studies in this area in the future and we will be happy to organize AUTOMATHEO Workshops also in the future.


Bruno Buchberger

Founder of the Research Institute for Symbolic Computation


Authors are encouraged to submit their four-pages extended abstract prepared in LaTeX, formatted according to the Springer llncs style no later than May 30.


Submission is web-based via this link:

Accepted papers will be published in a proceedings volume, which will be available during the workshop.

Workshop Program

The program is now available.