Buzzard said in his talk it took him 8 months and 30k lines of code to define one particular object he was interested in.
-
-
Replying to @littmath @jeremyjkun and
So to "check your work", because we can't prove BSD, will involve checking one example. This will involve formalising algorithms which compute the rank of an ell curve + proving that these algorithms are correct, and then analytically continuing the L-fn etc etc
0 replies 0 retweets 0 likes -
Replying to @littmath @XenaProject and
Yes, I'd be interested to hear about how you go about convincing someone who hasn't worked in Lean before that some object they understand well, but which requires a lot of work to formalize, is formalized correctly in that particular instance.
1 reply 0 retweets 0 likes -
Replying to @jeremyjkun @littmath and
Or even someone that has worked in Lean before :)
1 reply 0 retweets 0 likes -
Replying to @jeremyjkun @littmath and
speaking as a relative noob in Lean, it is generally not difficult to understand the statements of definitions / theorems in Lean; so provided you trust / understand the definitions that you see used (in my opinion no more problematic than doing so in "informal" math) ...
1 reply 0 retweets 2 likes
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.
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.