Message from Calculemus

July 30th, 2008 by Christine

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).

Message from MKM: Kantian Philosophy

July 30th, 2008 by Christine

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?

Message from MKM: Mathematical Exercises

July 30th, 2008 by Christine

There are multiple solution to a mathematical exercise:

Message from MKM: Mathematical Units

July 29th, 2008 by Christine

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)?

Message from MKM: Mathematical Methodology

July 29th, 2008 by Christine

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:

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

Message from MKM: Physics and Math

July 29th, 2008 by Christine

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”.

Message from MKM: Specifying Strategies of Exercises

July 29th, 2008 by Christine

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.

Message from CICM: Tagging and Annotating Proofs

July 28th, 2008 by Christine

See MathUI paper. Annotea-Extension for Proof Documents.

Message from MKM: An Update on Plato from the Omega Group

July 28th, 2008 by Christine

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)

Message from CICM: MathTran

July 27th, 2008 by Christine

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