Lean tooling and mathlib development as a career?

Stream: lean4

[Alex Keizer]

Sure, but is it possible to make a career out of working on that sort out stuff outside of academia? Are there companies interested enough in Lean that they're willing to pay for employees to work on such tooling?

[Martin Dvořák]

I think a crucial question is whether we can get paid for doing a work that we find meaningful but isn't viewed as a novel research.
I can, but it is because I am a Ph.D. student, hence I can do almost anything at this point in my life.
Can postdocs do this kind of work and get paid for it? Can professors do it as well?

[Martin Dvořák]

@Alex Keizer simultaneously :-)

[Martin Dvořák]

And I am asking not only about tooling!
Is the future of mathlib entirely dependent on volunteering?

[Arthur Paulino]

Alex Keizer said:

Sure, but is it possible to make a career out of working on that sort out stuff outside of academia? Are there companies interested enough in Lean that they're willing to pay for employees to work on such tooling?

I would search for companies that deal with critical software development. Like the ones building electrical cars, rockets, modern hospital equipment, systems that deal with large amounts of money etc etc

[Arthur Paulino]

There are software failures that can literally kill people

[Martin Dvořák]

Arthur Paulino said:

I would search for companies that deal with critical software development. Like the ones building electrical cars, rockets, modern hospital equipment, systems that deal with large amounts of money etc etc

Are they interested in building the basic tools tho? Or just the application that will secure their project, using existing well-established tools?

[Arthur Paulino]

I'd say it depends on the burden that older tools add to them. For example, some data scientists are starting to complain about the hegemony of Python APIs for developing advanced AI systems

[Alex Keizer]

I did have a look at ESA (the European Space Agency), and they are very much sticking with older, proven, tools (Ada) and huge amount of red tape. The aviation industry also follows mostly that philosophy, I think.

[Martin Dvořák]

Arthur Paulino said:

There are software failures that can literally kill people

How big part of the functionality of autonomous vehicles can be formally verified tho?

[Arthur Paulino]

I don't know, since I don't work on that field. But my optimistic guess is... at least the entirety of the circuit design?

[Arthur Paulino]

Alex Keizer said:

I did have a look at ESA (the European Space Agency), and they are very much sticking with older, proven, tools (Ada) and huge amount of red tape. The aviation industry also follows mostly that philosophy, I think.

So, what can Lean 4 offer that will help them profit?

[Martin Dvořák]

Can we maybe fork this discussion thread?

[Arthur Paulino]

Alex Keizer said:

Sure, but is it possible to make a career out of working on that sort out stuff outside of academia? Are there companies interested enough in Lean that they're willing to pay for employees to work on such tooling?

@maintainers sorry I don't know who to ping :sad:
Can we have a fork on this thread starting on that message :point_up: please?

[Mario Carneiro]

I think you can move messages

[Notification Bot]

15 messages were moved here from #lean4 > Feasability of creating a compiler in Lean by Alex Keizer.

[Alex Keizer]

Arthur Paulino said:

Alex Keizer said:

I did have a look at ESA (the European Space Agency), and they are very much sticking with older, proven, tools (Ada) and huge amount of red tape. The aviation industry also follows mostly that philosophy, I think.

So, what can Lean 4 offer that will help them profit?

Oh, I'm not saying they should use Lean instead, it would probably be a bad choice since Lean does not give them the desired control over memory layout. I suspect Lean would be a bad choice for most companies that deal with high-assurance software. It is simply too new, so anything that requires certification is already out, and a lot of the stuff you mentioned (cars, medical devices, rockets) deal with embedded software, which requires more control over the memory layout than Lean wants to give.

[Arthur Paulino]

Right, but then what's the opportunity you're aiming for?

[Martin Dvořák]

Martin Dvořák said:

And I am asking not only about tooling!
Is the future of mathlib entirely dependent on volunteering?

I think this question is also important. Should I move it to yet another thread? Or is there a short answer you can give me here?

[Alex Keizer]

To be honest, I'm still figuring that out myself ;).

My comments were mostly general philosophizing over the current state of PL development, and how general infrastructure work seems slightly underappreciated, rather than a concrete question about career opportunities.

To be fair, this is not a Lean specific problem. Rust is currently being lauded by a lot of industry players, and indeed funded, but I suspect that an embarrassingly amount of very crucial work on Rust is still being done by volunteers in their spare time.

[Arthur Paulino]

Martin Dvořák said:

Martin Dvořák said:

And I am asking not only about tooling!
Is the future of mathlib entirely dependent on volunteering?

I think this question is also important. Should I move it to yet another thread? Or is there a short answer you can give me here?

I'm not the most qualified person to answer this. But my guess is that mathlib may become a source of novel mathematical research someday. Then many doors would open up

[Arthur Paulino]

Alex Keizer said:

My comments were mostly general philosophizing over the current state of PL development, and how general infrastructure work seems slightly underappreciated, rather than a concrete question about career opportunities.

To be fair, this is not a Lean specific problem. Rust is currently being lauded by a lot of industry players, and indeed funded, but I suspect that an embarrassingly amount of very crucial work on Rust is still being done by volunteers in their spare time.

One of the challenges is that companies pay for products or services. So if you're not working on their products directly, then it's hard to qualify your work as a service for them.

Society, however, clearly needs better investments in tech infra. And the academy doesn't have nearly enough bandwidth for that

[Arthur Paulino]

Companies make millions of dollars on top of Python, Javascript, databases and many other free tools. The question is, how to develop free/open tools in a sustainable way? Namely, one way that allows you to pay your bills etc

[Martin Dvořák]

My impression is the following (please prove me wrong):

PRIMARY RESEARCH
You can do it in academia. If you publish enough papers, you will make a good career there.

APPLIED RESEARCH
There is a huge demand for it in both academia and industry. There are many career opportunities.

APPLIED ENGINEERING
There is a very huge demand for it in industry. People who do it aren't worried about getting their bills paid.

PRIMARY ENGINEERING
Who pays for that? Clearly, Microsoft paid for the development of Lean. However, there is much more to be done. And I don't see how to make it a part of one's academic career or industrial career. Is it then left upon volunteers?

[Arthur Paulino]

I don't know what you mean by "primary" vs "applied"

[Martin Dvořák]

In our context: Primary research would be developing novel tactics for Lean. Applied research would be discovering what properties of computer-vision algorithms can be formally verified. Primary engineering would be reimplementing a powerful Coq tactic in Lean. Applied engineering would be verifying the correctness of a concrete piece of electronics or software for a car.

[Martin Dvořák]

The line between primary research and applied research is very blurry in my head. However, I am concerned about the striking difference (in career opportunities) between applied engineering and primary engineering. Who will pay people that port the best features from other theorem provers to Lean?

[Arthur Paulino]

Maybe this way of thinking is inverted. It would have to start from the company itself. It would have to come from a team that already makes a profit out of software verification

[Martin Dvořák]

Arthur Paulino said:

I'm not the most qualified person to answer this. But my guess is that mathlib may become a source of novel mathematical research someday. Then many doors would open up

You mean the far future when interactive theorem provers will become so convenient to use that a new mathematical research (never done on paper before) will be done in Lean or similar systems?

[Martin Dvořák]

Then I am worried that the future of mathlib is heavily dependent on volunteering.
We cannot get a paper out of proving thousands of little lemmata.
And there is no industrial interest in having the entire body of mathematics formalized on computer one day.

[Arthur Paulino]

Don't take my word for it. There are more reasons to formalize maths. Pedagogical reasons, even

[Martin Dvořák]

I am worried there is no skip-to-the-good-part button.

[Martin Dvořák]

Arthur Paulino said:

Don't take my word for it. There are more reasons to formalize maths. Pedagogical reasons, even

Sure. But can full-time lecturers decide to teach less lessons per week in order to invest worktime into formalizing basic MathematiCS (that will not get published in journal/conference) ?

[Martin Dvořák]

My guess is NO. Therefore, in order to contribute to mathlib, they would either have to spend their free time (evenings, weekends) on formalization or partially neglect students in their worktime.

[Arthur Paulino]

Sorry, that's really out of my league. We have well-established professors here so they would provide better input on this. But I wouldn't be surprised if you just hit the nail on the head

[Martin Dvořák]

I am, as a Ph.D. student, in a somewhat privileged position — I can do all week whatever I want to do and nobody will punish me for it.

Yet still, my supervisor clearly tells me not to spend time on stuff that has no potential for publication. And I more or less follow the instruction.

[Arthur Paulino]

In my (naive?) understanding, though, a living and up-to-date body of formalized mathematics is something that human beings will achieve someday. It's a matter of time

[Martin Dvořák]

PS: I wanted to move my tangent elsewhere, but I cannot move it to a new topic outside of the lean4 stream, so I will keep it here. Sorry for OT.

[Martin Dvořák]

Arthur Paulino said:

In my (naive?) understanding, though, a living and up-to-date body of formalized mathematics is something that human beings will achieve someday. It's a matter of time

This isn't reässuring enough for me. Will we achieve it during my lifetime? Will we achieve it before we destroy this planet? I have these concerns when I think about the big picture.

[Alex Keizer]

Martin Dvořák said:
[...] Will we achieve it before we destroy this planet? I have these concerns when I think about the big picture.

If that is your concern, it seems like we should strife to delay the latter, rather than speed up the former ;).

Jokes aside, I agree with the sentiment. A lot of this work, be it tooling, be it formalizing existing mathematics is necessary before we can get to to good, truly novel, stuff. It seems weird to me that we don't make sure there are incentives to do it, rather than relying on volunteers.

[Alex Keizer]

Martin Dvořák said:

I am, as a Ph.D. student, in a somewhat privileged position — I can do all week whatever I want to do and nobody will punish me for it.

They might not punish you directly, but if you do spend most of your time on non-publishable work, won't that affect your further career prospects? So the incentive to not work on primary engineering is still there, right?

[Jireh Loreaux]

Martin Dvořák said:

Arthur Paulino said:

I'm not the most qualified person to answer this. But my guess is that mathlib may become a source of novel mathematical research someday. Then many doors would open up

You mean the far future when interactive theorem provers will become so convenient to use that a new mathematical research (never done on paper before) will be done in Lean or similar systems?
Then I am worried that the future of mathlib is heavily dependent on volunteering.
We cannot get a paper out of proving thousands of little lemmata.
And there is no industrial interest in having the entire body of mathematics formalized on computer one day.

I'll point out that there has already been new mathematical research done in Lean, at least in some way with the recent work of David Ang and Junyan Xu in this thread on elliptic curves where they provide a proof of associativity of the group operation in arbitrary characteristic with a unified approach that isn't just "do a gigantic computation", which, as a I understand it, is entirely new. I'm not claiming that associativity wasn't proven in all characteristics before, just that it wasn't done with a single unified proof technique. This is mathematically interesting and (I believe) warrants a paper on the topic even separate from its formalization.

I think improving proof techniques and unifying approaches will be one of the first mathematically salient fruits of interactive theorem proving before we get to some state where ITP actually helps us prove mathematically new results.

[Kevin Buzzard]

I think that you can prove associativity with a single unified proof technique using Picard groups and some algebraic geometry

[Jireh Loreaux]

Ah, then I misunderstood. Nevertheless, it's still cool. :smiley:

[Kevin Buzzard]

The Ang-Xu proof uses far less machinery, for sure.

[Martin Dvořák]

Alex Keizer said:

If that is your concern, it seems like we should strife to delay the latter, rather than speed up the former ;).

I could also reverse the concern... What if formally-verified MathematiCS is what will help us to escape from the nest before we burn it down?

[Wojciech Nawrocki]

One perspective on academia and software development was given here by William Stein, the principal developer of SageMath. TL;DR: he became frustrated enough with academic crediting to quit.

[Eric Wieser]

Alex Keizer said:

To be fair, this is not a Lean specific problem. Rust is currently being lauded by a lot of industry players, and indeed funded, but I suspect that an embarrassingly amount of very crucial work on Rust is still being done by volunteers in their spare time.

From experience outside Lean, sometimes paid positions do come up to continue to work on open-source projects; either within companies that use the software, or more rarely as non-profit funding. In the former case you'd presumably end up at the whim of the company deciding your skills are more useful on something proprietary, while the latter tends to only be a short term option.

[Julian Berman]

If further non-Lean anecdotes are helpful, I'm personally thankful to have thus far avoided even "ending up at the whim of the company deciding your skills are more useful on something proprietary" -- I still manage to be graciously paid to work on open source all day long simply because the company recognizes those projects to be valuable. Perhaps it's rare, but thankfully it happens! One would definitely hope some day the same would be true for Lean/mathlib/etc.