“KWARC was!”

James Davenport’s plea for providing more insights on the proof and how one got it done and … if a computer can’t solve it, is it really not provable. Shouldn’t it rather return “I can’t solve it”?

An interesting comment wrt. to the fact that William Farmer and Alan Bundy pointed me to, that is that the way mathematicians present and illustrate a proof (in publications, books, and even lectures) is not the way we actually retrieved the proof.

And it contributes to another interesting discussion, that is whether or not trusting and accepting automatically computed proofs (see the Flyspeck project).

Aaron Sloman: Talk is online. His work also emphasize the need of not enforcing representation and practice but taking existing evolutions and, in particular, philosophy into account. So is this a motivation for me to look at mathematical philosophy for understanding mathematical practice?

There are multiple solution to a mathematical exercise:

• 8 ways for Three by One
• Different numbers of proving steps: see MKM: Specifying Strategies of Exercises

James Davenport gave a talk on mathematical units in OpenMath.

New to me was the discussion on whether and when CDs/ units/ notations are obsolete (e.g. out-of-date)

• OpenMath CD is obsolete if the definition in it are for archival purposes only.
• A unit is obsolete by formal change (e.g. liter_pre1964) and by usage.

Or to distinguish relative and absolute temperatures … for addition “abs”+”rel”=”abs” (not arith1-plus?) …

Units are also very interesting in making mathematical expressions more intuitive and context-dependent. Maybe: A renderer converting from 1.2 miles (English) to (ca.) 1,92 km (German) should also convert the units and thus needs to provide basic computations (e.g. from miles to km)?

William Farmer pointed me to an interesting point that I have so far not considered:

The way mathematicians present their work does not necessarily reflect the way the do math. These are two very different aspects of mathematical practice: The practice mathematicians (commonly) develop/ use to present their work and the practice they apply to do math (to solve mathematical problems). Consequently, limiting my analysis of practice to literature (mathematical results) and the included notation will not allow me to fully understand practice. Instead, I would need to observe and interview mathematicians to understand the way of doing math … or even start attending fundamentally math lectures (e.g. an abstract algebra course) and become a mathematician myself.

Mathematical text books worth while reading:

• Caculus (Michael Spivak)
• Algebra (Larry C. Grove)

In addition to mathematical text books, there is some (more philosophical) literature out there that can help to understand practice

• George Polya: How to solve it!
• Imre Lakatos: Proofs and Refutations
• Thomas S. Kuhn: The Structure of Scientific Revolutions
• Karl Popper: The Logic of Scientific Discovery
• Bettina Heintz: ie Innenwelt der Mathematik. Zur Kultur und Praxis einer beweisenden Disziplin

Some links, not all of them yet evaluated

• Listing Examples for the Methodology of Math citing P. Davis and R Hersh books “The mathematical experience” and “Descartes’ dream”.

Joseph Collins presented a Mathematical Model of the Physics Modeling Process and discussed the representation of Physics. He emphasized that semantics of objects vary in math and physics: For example,

• a physical field versus a mathematical field

See MKM 2008 proceedings “A mathematical type for physical variables”.

Johan Jeuring presented me their tool for incrementally solving exercises. The system provides a progress bar, feedback, and hints as well as verifies each step (so providing immediate feedback to the students). For each assignment one has to find a problem domain i.e. “simplifying fractions” and define the respective mathematical domain and a strategy for the type of problem.

For my work on mathematical practice this is extremely valuable, since their work observes and explicates ways of solving mathematical problems. In order to get the respective strategies they ask a mathematical specialist to explain them.

See MathUI paper. Annotea-Extension for Proof Documents.

Very interesting approach. They take our notation-rendering approach on the level of documents, i.e. presentation markup is interpret wider and includes narrative presentation markup:

Plain text documents are first structured and verified; missing proof steps are propagated to the initial document and, in particular, “rendered” into the “plain text presentation”.

For CoPs it would be interesting to analyze different proofs wrt. the level of detail.

See MKM Proceedings: Authoring verified documents by interactive proof construction and verification in Text-Editors. (Dominik Dietrich, Ewaryst Schulz, Marc Wagner)

Jonathan Fine focuses on capturing and improving large amounts of materials.

MathTran is a public web service and samples. Display on webpage is based on img tags and Javascript. Instant Previews. Coping with the breadth; instead of doing much with little amounts of content (breadth).

See paper