And do they get tenure- or funding-able output of it, or is it more of a side-hobby?
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.
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.
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.
[1] https://www.unco.edu/nhs/mathematical-sciences/faculty/mille...
It was a project in which we formalised a version of Gromov's (open, ample) h-principle for first order differential relations. Part of the reason it was carried out was to demonstrate what is involved formalising something in differential topology.