Lean Jobs that don't need a PhD

Stream: new members

[LordRatte]

I noticed that almost all job postings in the #job postings channel require academic background or is just contracting work.

I'm an engineer with 15 years experience in a few languages. I enjoy maths and most of what I know comes from self study. I've never published a paper before (although I would love to contribute to one some day). Mathematically logic comes naturally to me but there is certainly a lot I still have to learn.

Is there a place for someone like me in the full-time Lean job market? And if so, where do I connect with my potential future employers?

[Code Apprentice]

Sounds like you are in a similar place as I am. I don't have any answers for you about how to get a job in Lean. Just want to post my support. I am also an software engineer. I am learning Lean4 on the side as a hobby. Very intrigued by using it for formalizing mathematical theorems.

[Shreyas Srinivas]

Honestly, the answer is probably “very few” if you exclude those dataset creating contractual roles. You still need to be deep into math or formal verification or the internals of theorem provers + their theory to be able to make meaningful contributions. There might be a few roles focussed on tooling and engineering support, but those seem rare and only exist at places like the Lean FRO itself or the mathlib initiative.

[Shreyas Srinivas]

People do pick up ITPs and use them as stepping stones to get deep into the topics I mentioned, even if they are from outside academia.

[Shreyas Srinivas]

But it takes extraordinary effort to make the kind of contributions that stand out. The few people I know who did that eventually started PhDs.

[Shreyas Srinivas]

That being said, lean is still short on the libraries front for doing system tasks. It doesn’t have a web framework for example. It doesn’t have a great CAS system built in it. There are experimental projects for writing numerical algorithms (Scilean) but they are still a WIP. So maybe there is still a bunch to be done on the software libraries side of lean. I just don’t know too many employers paying for this to happen other than the FRO.

[LordRatte]

@Shreyas Srinivas I see. Very few is what I was expecting to hear but I thought it would at least be worth asking.

[Oliver Nash]

I've been on both sides of hiring quite a bit over nearly 20 years and my advice is that a job ad is always a description of the dream applicant.

Of course you shouldn't waste people's time with highly speculative applications, but if you really do have good relevant skills and knowledge but don't tick some box (e.g., PhD) then this should not stop you from applying.

[Kevin Buzzard]

If you want to beef up your CV then I would start contributing to the open source projects out there in your area e.g. perhaps CSLib or Mathlib? Certainly when I was hiring recently I was looking for public examples of competent Lean code written by applicants.

[František Silváši 🦉]

IME (purely anecdotal from the industry; in academia, which is still a majority of Lean jobs, it's different):
It's more often than not the case that we hire 'someone we know of' from the community - so participating (e.g. contributing to open source, published Lean work, etc.) is borderline necessary. PhD. has nothing to do with the job requirements; it just so happens most people do have one, but that's because they're more likely to have participated in the community.

Most industrial Lean-adjacent players I meet are the same - they're not explicitly looking for people with a phd. so don't let this deter you at all, unless you're fishing for an academic position.

[LordRatte]

This is helpful feedback all around. Thank you all.