Yes, they get grants to work on it. Other questions? I can't say I enjoy this "gotcha" tone.
Compare these two cases:
> people who use or contribute to lean
And do they get tenure- or funding-able output of it, or is it more of a side-hobby?
> people who use or contribute to lean
Do they get tenure- or funding-able output of it, or is it more of a side-hobby?
The "And" at the begining makes it snarky to me. It's probably just me tho.
Do most working mathematicians use proof assistant or checkers? Does anyone have a percentage with feedback on how they use them?
FWIW, the industry term for this is "dogfooding", and it's usually seen as a predictor of high quality tool.
For the original question, a survey might want to separate these two. One just says people are working on a product. Why could be any reason, like just making money. People using it, but not paid to, are more valuable as reviewers.
I really have no idea why people are taking this approach here.
Proof assistants are useful. People use them to do actual maths. There is a lot of work to formalise all of maths (this isn't a proof assistant thing this is a huge undertaking given maths is 3000+ years old and we've only just decided what formality really fundamentally consists of) so some places you need to do more foundational work than others to make it useful.