xQuant

I have been looking a long time for a way to represent on the web a mathematical corpus. It would be tremendous if one could find on the web the different books written on a subject, in a form that enables verification of theorem and proof.

Let’s reflect on what a lesson is. Mostly a lesson is about learning one by one different entities, and the relations that those entities share. It is all about serializing a graph.

If we were to improve this process of learning, we should identify what represent the most effort and the least added value in the making of it, and I see 3 big bottleneck.

- This process has to occur at a level the audience can understand. The same lesson can take a day or 5 minutes depending on the knowledge of the audience. One of the big problem that clutters reuse of lessons on a large scale basins is that every time one wants to adapt the level, a whole rewrite is necessary.

Having a formal representation of books would allow for seamless rewrite of proof down to the basic axiom if necessary.

- Another variability is how does one reuse the theorem or presentation of another. Dissemination now is informal, slow, and based on individual reading. Few ways exists to have clever solution to emerge. A repository of steps for proofs, which would allow reuse in other context, would enable indirect voting, and promote the best practices.

- Finally, another problem is the sheer size of the domain which can only be tackled with by many specialists. Sometimes the difficulty lies not in the domain itself but in the many ways there are to show one same effect. There is no place for such collaboration to take place in a fruitful way, with people ranging from high school students to phd’s to contribute and enrich each other. Sure, wikipedia exists, but is completely out of scope : what if I was to see the 10 differents ways to prove an assertion, and how the theorems used apply in the specific case i am looking at ? wikipedia can’t handle this kind of data explosion and no onewill contribute this to the details I might need (and some other person won’t)

So, facing those issues, one might think that the computer science people in universites found a way ? No, you want to know why ? They are research ways not tho share proof and have a formal system for proof and representation. no. they are waaaaayy behond that : they are looking to automate the creation of proof.

This really is for me the completely wrong way to go, and we should first concentrate on having a formal description system to tackle those 3 points I exposed. Then, with such a useful formal description, will we get ammo for automated proof, if we ever can solve it.