Workshop on
Mathematically Intelligent Proof Search
MIPS 2010
Paris, France, 10th July 2010
The workshop on Mathematically Intelligent Proof Search explores the
relationship between mathematical theory development and proof construction.
It aims most directly at taking steps towards a deeper understanding of this
relationship in both informal and formal contexts, but has the central,
longterm goal of bringing these two contexts closer together in a
systematic way. This would pave the way for having machines analyze
mathematical texts and uncover leading ideas or heuristics for parts of
mathematics.
In either context, theory development and proof construction are deeply
connected: the choice of a language, expanded by definitions, and of a
corresponding inference mechanism correlates with how effectively proofs can
be obtained and how well mathematical arguments can be communicated. Thus
languages can range from mathematical vernaculars that are close to natural
languages to purely formal ones; inference mechanisms can structure
arguments conceptually but may also be based on automated proof procedures
that are mathematically intelligent.
MIPS will bring together researchers from Computer Science, Linguistics,
Mathematics and Philosophy who are interested in the whole subject or parts
of it, in order to get an overview of the state of the art, present original
results and discuss directions for future research:
The scope of MIPS thus includes topics such as
 formalization and automated proof search for mathematical
theories:
 domains of specific interests are set theory and geometry
 interactive verification and automated proof search
 alternative formalizations and their adaptive selection


 analysis and generation of mathematical texts
 natural language vs. controlled natural language
 domain specific vs. generic lexika text analysis
 textlinguistic aspects of mathematical texts
 cognitive aspects of the conceptualization and representation of mathematical texts
 adaptive document generation styles

with practical applications for
 authoring of mathematical texts
 verification of mathematical documents
 dynamic proof tutoring in mathematics
We encourage researchers working at points of contact among these
fields to share their views, work, or results by submitting a
title and abstract or short paper (25 pages in PDF format) and
taking part in the workshop. Please submit your work via EasyChair
http://www.easychair.org/conferences/?conf=mips2010.
Any questions you may have about the workshop should be send to mips2010@easychair.org
Submission of title and abstracts:  June 18, 2010 
Notification of acceptance:  June 24, 2010 
The accepted work should be presented at the workshop, which will
be a mixture of invited and accepted presentations. The
abstracts/short papers of the accepted and invited presentations
will be collected in informal proceedings and made available at
the workshop.