Topic: FABSTRACTS funded
Kevin Buzzard (Mar 28 2018 at 15:31):
Andrew Ashworth (Mar 28 2018 at 15:43):
metric #4 seems ambitious
Andrew Ashworth (Mar 28 2018 at 15:44):
but perhaps the people behind fabstracts are such big shots that thousands will pick up a proof assistant and get cracking
Andrew Ashworth (Mar 28 2018 at 15:46):
this is quite exciting though, i'm for anything that gets people interested in formal verification
Gabriel Ebner (Mar 28 2018 at 16:18):
That's like 5 uses per day. "We define a use as a visit to our website or a git clone of the fabstracts repository." (Note: that's how I would write the project report.) Sounds perfectly doable.
Sebastian Ullrich (Mar 28 2018 at 17:00):
Sounds like perfectly doable by Travis alone
Kevin Buzzard (Mar 28 2018 at 17:10):
Mathematicians need to be trained, but I hope to put together some sort of maths version of Software Foundations this summer. I don't see anything stopping mathematicians from using Lean to formalise their abstracts other than the learning curve, which is what I hope to help people get over. Also the mathematical community needs to start training its undergraduates, or at least give them access to the the resources so they can train themselves.
Kevin Buzzard (Mar 28 2018 at 17:11):
I guess another issue is that mathematicians will need the definitions which they're accustomed to working with. But I guess this is where some of the money will go, into getting people to formalise a bunch of definitions.
Kevin Buzzard (Mar 28 2018 at 17:13):
Failing that I'm pretty sure you can buy thousands of clicks easily nowadays. My kids were all on Instagram when they were about 14, and most of their friends had 30 followers but one kid had over 1000 followers because he bought them.
Kevin Buzzard (Mar 28 2018 at 17:14):
Maybe Hales can use some of the money to do that.
Last updated: May 18 2021 at 16:25 UTC