FABSTRACTS funded

Stream: general

[Kevin Buzzard]

https://jiggerwit.wordpress.com/2018/03/28/formal-abstracts-in-mathematics/

[Andrew Ashworth]

metric #4 seems ambitious

[Andrew Ashworth]

but perhaps the people behind fabstracts are such big shots that thousands will pick up a proof assistant and get cracking

[Andrew Ashworth]

this is quite exciting though, i'm for anything that gets people interested in formal verification

[Gabriel Ebner]

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]

Sounds like perfectly doable by Travis alone

[Kevin Buzzard]

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]

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]

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]

Maybe Hales can use some of the money to do that.