well you have someone read it, for one. and now they just have to verify that the definitions correspond to what is claimed. hales' current project for a "library of math" includes a notion of reviewers and certifications that the formal statements correspond to those written.
-
-
it is not too hard to see whether what's *stated* is what you have in mind. (Though just as in informal math, this may require chasing down some dependencies...) Understanding what precisely is going on in the code in the *proofs* is of course much harder.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.