I have the feeling that the challenge of bringing mathematicians and computers closer together, requires a lot of expertise in the field of pure mathematics and the more technical-field of mathematical knowledge management. The latter requires a good overview on mathematical tools, in particular, computer algebra systems and theorem provers as well as other mathematical editors (e.g. Plato). Moreover, the step-wise formalization of mathematical text seems to be a core interest and competence of the whole KWARC group rather then my own research focus.
Looking at the discussion with Cris on the confidence in proofs, acceptance of proofs as well as trust in proofs, I am wondering, whether we could use our understanding of the mathematical practice and use it for providing an assessment and reputation system for mathematics, i.e. something that we could attach onto a repository of mathematical knowledge and use to facilitate the collaboratively assessment of the mathematical community on different layers:
- Is (the proof) published in journals (considering the impact factor of these journals)
- Was it accepted by the Zentralblatt or Mathematical Reviews (adding more confidence)?
- How long was the proof tested by the mathematical community?
- How many proofs do exist for the theorem?
- Is it a nice proof/ theorem (beauty)?
- Is it correct? (later adding automatic verification methods …)
- Can it be understood (e.g. measured by the numbers of references and re-uses)? How hard can it be understood?
- Is it re-used by the community, i.e. is it relevant and useful for further mathematical work?
We can imagine a top-down and bottom-up approach:
- The top down approach requires the user’s explicit assessment of the content: evaluating the users’ ratings, tags, bookmarks
- The bottom up approach could implicitly provide the relevance of content making use of the logical and narrative structure of the mathematical knowledge: computing theory interrelations, citations, …
I will discuss with Cris, whether he thinks that this would lead to a useful application for mathematicians.