I’m now at MKM2007 whose book[1] has the splendid title:
Towards Mechanized Mathematical Assistants
the vision that computers can work together with humans to enhance the the understanding of both parties. This vision has much in common with our own SciBorg project where we use the idea “scientist’s amanuensis” for a computer system than can help hi=umans understand chemistry in machine-accessible form
(see also An Architecture for Language Processing for Scientific Texts)
As with many of my talks I’m blogging so of the talks – ans more importantly the encounters – during this meeting. I haven’t decided what I’m going to say tomorrow and these notes may form part of it.
I’m first of all searching for similarities in the thought processes between the MKM community and our own chemical knowledge community (i.e. those people in chemistry who have realised we are in the Century of information and knowledge – a small percentage). That’s also true in mathematics – the MKM community – which overlaps with symbolic computation and computer algebra – is not mainstream but, unlike chemistry, has achieved critical mass (i.e. there are regular meetings, serial publications, etc. – that’s a pointer for ourselves – we need to do these things as well). So here are some top-level isomorphisms:
- need to check the correctness of submitted manuscripts. Maths has many places where the author states “it’s obvious…”, or lemma 12.23.34 appears without an actual derivation. In chemistryand other sciences we have suspect or missing data
- it’s not “proper maths/chemistry”. Markup is trivial/non-essential/notRealResearch, etc. You have to proves theroems or make compounds to be a proper researcher.
- The Open Source systems are no good because the commercial systems (Mathematica, Maple, ChemDraw, OpenEye) are better. If it doesn’t cost money it can’t be any good
- Machines can never have the insight that humans have.
- The publishers/senior editors know what is good for the community. We’ve done in on printed papaer for 200+ years. It works, whyc change it? (It’s also a lot of trouble.
The first lecture (Paule) showed that machines can now prove some quite complex theorems. Cerianly miles beyond me. Things like Wallis’ formula for PI and Ramanujan’s first identity. And, if we are going to use symbolic algebra systems, we need other systems to prove that the CAS are correct.
[1] Springer, LNAI 4573 eds: Kauer, Kerber, Miner, Windsteiger. Not, of course, Open Access – you have to buy a physical book.