15 ms·
> 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?
by shakow 2y ago
> 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?
- g15jv2dp 2y agoYes, they get grants to work on it. Other questions? I can't say I enjoy this "gotcha" tone.
- Jensson 2y agoSo they get grants to work on these tools rather than to work on math, seems like a very special situation then and a very special math department and therefore not a good picture for how helpful it is to math departments in general.
- nimih 2y ago"No true working mathematician would spend their time using Lean!"
- g15jv2dp 2y agoI guess we got in the top 10 worldwide for math in the Shanghai ranking by accident. If you don't know what you're speaking about, sometimes it's wise to not say anything.
- seanhunter 2y agoThe mathematicians I know of who work on Lean4 as part of grant-funded research do so because their research funding is for formalising mathematics and Lean4 is the tool they choose to use for that. 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.
- szvsw 2y agoIsn’t working on these tools a form of working on math? Math is a language unto itself.
- nickpsecurity 2y agoI’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?
- TeMPOraL 2y 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.
- nickpsecurity 2y agoThere’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.
- GPerson 2y agoThe person you are replying to asked a very useful question, and you supplied a useful answer. I don’t detect any snarky tone in their comment.
- raincole 2y agoIt sounds quite "gotcha" to me. 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.
- shakow 2y agoThat's not a “gotcha”, but an interrogation on whether what I experienced in bioinformatics (i.e. working on tools, especially already existing ones, is a carreer trap) also applied to maths.
- a_wild_dandan 2y agoSnark and contrarianism are specialties around here. Thank you for sharing your experience; I genuinely appreciate it.