I am sitting in Robert Miner’s (Design Science) talk on Mathdex in MKM2007, he is stressing that the most imporant thing in in their experiments turned out to be data normalization. He is actually going a long way towards semantics for the general case. At least he is generating some kind of trees, so we will be able to index them in the MWS system. They are interpretable in first-order terms, which is all that MWS needs. It would be very nice if we could build on the idea we had last MKM to have a set of challenge examples that we all can work on and compare our systems.
Archive for the ‘MKM’ Category
Treating Mathdex Presentation trees for MathWebSearch
Saturday, June 30th, 2007MKM for Tom Hales’ Proof Text
Friday, June 29th, 2007I am sitting in Tom Hales Talk at MKM 2007, where he discusses how he is re-arranging his 1998 proof of the Kepler conjecture in a way so that it becomes more palatable to formalization process (the flyspeck project). He says that the proof text is becoming much less dense in the process.
This seems like a very good case study for MKM, most particular the SWIM semantic Wiki for Math, together with Normen’s Change managment techniques (see Locutor).
I think that I will ask him for access to the text as a case study.