I find Bret Victors talks quite inspiring and would love to collaborate with him on interfaces for collaborative mathematics. I think he is misguided though on

I find Bret Victors talks quite inspiring and would love to collaborate with him on interfaces for collaborative mathematics. I think he is misguided though on the "Kill Math" angle. There are two different kinds of maths. 1) The well-understood one, and for this kind of math there should actually exist much better interfaces for it than the "freakish manipulation of abstract symbols". 2) The new one, where you are not sure about your concepts yet etc. For the new one it is ALSO (maybe even more so?) important to be able to approach it via (virtual) physical experiments / models, but in the end the new territory has to be mapped out by symbols. By logic. Only then the full power of math can be realized. But of course there is no reason why working with logic should NOT be supported by the computer; actually I would think the computer is ideally suited to help with that task.