Math, Proofs, and Collaboration
December 15, 2013
I know that the search engine optimization folks already are on top of this idea, but for the mere mortals of the “search” world, check out “Voevodsky’s Mathematical Revolution.” Vladimir Voevodsky is a Fields winner and he was thinking about some fresh challenges. He hit upon one: The use of a computer to verify proofs. The write up explains a “new foundation is that the fundamental concepts are much closer to where ordinary mathematicians do their work.”
The comment I noted pertains to mathematical proofs. As you know, creating a proof is, for many, mathematics. However, verifying proofs is tough work. The quote I noted is:
“I can’t see how else it will go,” he said. “I think the process will be first accepted by some small subset, then it will grow, and eventually it will become a really standard thing. The next step is when it will start to be taught at math grad schools, and then the next step is when it will be taught at the undergraduate level. That may take tens of years, I don’t know, but I don’t see what else could happen.”
The consequence of automated methods like Coq is even more interesting:
He also predicts that this will lead to a blossoming of collaboration, pointing out that right now, collaboration requires an enormous trust, because it’s too much work to carefully check your collaborator’s work. With computer verification, the computer does all that for you, so you can collaborate with anyone and know that what they produce is solid. That creates the possibility of mathematicians doing large-scale collaborative projects that have been impractical until now.
Interesting.
Stephen E Arnold, December 15, 2013
Comments
One Response to “Math, Proofs, and Collaboration”
-
- Subscribe to Beyond Search
Feature archive
News archive
-
klik