Can the formalization of mathematics be performed by mass effort of huge numbers of not-brilliant people not working in coordination?
The idea is it doesn't matter how ugly the proof is so long as it is correct, and correctness can be checked by the proof assistant or interactive theorem prover. All the individual proofs are put into a giant database, available for anyone else to use as a lemma. The key technology still needed is to be able to search for the lemma you need.
Let these be the puzzles you work on in your spare time. Unproved (unformally) theorems come out of a dispenser. In principle, the hard part has already been done, in natural language, so all that remains is translating it so a computer can understand.
Will it be great? That is, if enough gets completed, will it snowball into something with more practical or significant? Or is it just retreading old ground? After all, everything is built on mathematics.
No comments :
Post a Comment