Hacker News new | ask | show | jobs
by nickpsecurity 734 days ago
I’m with them. They’re using a tool they’re paid to work on. That’s always a special case. The general case would be what percentage of mathematicians use (a) proof assistants at all, (b) mechanized proof assistants, and (c) Lean specifically.

Do most working mathematicians use proof assistant or checkers? Does anyone have a percentage with feedback on how they use them?
1 comments
TeMPOraL 734 days ago
> They’re using a tool they’re paid to work on. That’s always a special case.

FWIW, the industry term for this is "dogfooding", and it's usually seen as a predictor of high quality tool.

link
nickpsecurity 733 days ago
There’s two issues here: getting paid to work on a product; using the product yourself. People often do one without much of the other. People dogfooding do both.

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.

link