In my PhD work, I studied mathematical proofs, taken from Hardy & Wright's textbook on Elementary Number Theory, with the goal to build a system that converts the informal input into a formal proof representation structure.
The best references for this work are:
C. Zinn.Understanding Informal Mathematical Discourse. PhD thesis, Institut für Informatik, Universität Erlangen-Nürnberg, September 2004. Published as:Arbeitsberichte des Instituts für Informatik, Band 37, Nr.4, ISSN 0344-3515. Understanding Informal Mathematical Proofs. pdf
C. Zinn. A computational framework for understanding mathematical discourse. Logic Journal of the IGPL, 11(4):457–484, 2003. link
C. Zinn. Supporting the formal verification of mathematical texts.Journal of Applied Logic, 4(4), December 2006. doi
My PhD thesis and minor publications (workshop proceedings) are given below. Let me know whether you are interested in receiving a hardcopy of my thesis or journal offprints.
C. Zinn. Understanding Informal Mathematical Discourse. PhD thesis, Institut für Informatik, Universität Erlangen-Nürnberg, September 2004. Published as: Arbeitsberichte des Instituts für Informatik, Band 37, Nr.4, ISSN 0344-3515.
C. Zinn. Understanding Mathematical Discourse. In Proceedings of Amstelogue’99 Workshop on the Semantics and Pragmatics of Dialogue. Amsterdam University, 1999.
C. Zinn. Computing Presuppositions and Implicatures in Mathematical Discourse. In Proceedings of the 2nd. Workshop on Inference in Computational Semantics (ICoS-2), pages 121–135. Schloss Dagstuhl, Germany, 2000.
C. Zinn. Conditionals and pseudo-conditionals in mathematical texts. In Proceedings of the 4th. Workshop on Inference in Computational Semantics (ICoS-4), pages 217–232, Nancy, France, 2003. LORIA.
C. Zinn. Parsing formulae in textbook proofs. In Proceedings of the 3rd. Int’l Workshop on Computational Semantics (IWCS-3), pages 422–424. Tilburg University, 1999.
C. Zinn. On the use of variables in mathematical discourse. In E.Buchberger (ed.): Proceedings of Konvens 2004 (7. Konferenz zur Verarbeitung natuerlicher Sprache), ISBN 3-85027-005-X. Lecture notes series of the Austrian Society for Artificial Intelligence, Vol. 5, pages 217–220, Wien, 2004.
C. Zinn. Towards the Mechanical Verification of Textbook Proofs. In Proceedings of the 7th. Workshop on Logic, Language, Information and Computation (WOLLIC-2000), pages 201–211. Natal, Brazil, 2000.
