Are there many Lean users now?

Stream: general

[(deleted)]

I just saw that there are 1000+ applications for the Axiom Math job posting. #job postings > Axiom Math Update - Thank You

Does it mean there are now tens of thousands of Lean users now?

[(deleted)]

But it's odd. Writing proofs is hard. How can there be so many Lean users out there?

[Yaël Dillies]

The Axiom Math job posting isn't only about Lean experts, they are also hiring ML engineers (which are much more common), it seems

[Michael Rothgang]

This zulip channel has 12.000 users now. If each of them used Lean at some point, I guess that means a yes.

[Michael Rothgang]

And I believe a lot of Lean users are not on zulip or not even active --- so it's hard to estimate who's also out there.

[Henrik Böving]

https://marketplace.visualstudio.com/items?itemName=leanprover.lean4 We know that the extension has been downloaded almost 90k times

[Yaël Dillies]

But does that count my 80k gitpod workspaces? :innocent:

[Shreyas Srinivas]

Gitpod downloads from open-vsx

[Shreyas Srinivas]

As do alt-vscodes

[Yaël Dillies]

Does that mean it's counted above, or not counted above?

[Shreyas Srinivas]

The vscode marketplace count only shows those who installed the application from within vscode (internally it also shows us those who “downloaded” it from the marketplace, which I think includes using the cli to install it or just installing from the vsix onto alt vscode editors)

[Shreyas Srinivas]

Yaël Dillies said:

Does that mean it's counted above, or not counted above?

Gitpod uses won’t show up on the marketplace.

[Yaël Dillies]

Then that 90k is truly impressive

[Shreyas Srinivas]

Also on open-vsx your contribution to the count will be only 1

[Shreyas Srinivas]

Keep in mind that this includes people who have multiple machines. It includes all those who installed it on a workshop or a seminar course and never touched lean again. It includes my two or three dozen virtual machines that I had at some point with the lean extension installed.

[Shreyas Srinivas]

It doesn’t tell you how many people actively use lean.

[Shreyas Srinivas]

Even if only 20% of those downloads come from active users, that is still impressive.

[Shreyas Srinivas]

And that wouldn’t include people who use lean with cursor or vscodium.

[Marc Huisinga]

Yaël Dillies said:

Then that 90k is truly impressive

The OpenVSX extension has 40k installs, by the way: https://open-vsx.org/extension/leanprover/lean4

[Eric Wieser]

So 30% of Lean users are using gitpod?

[Marc Huisinga]

I don't have any data on that, unfortunately :-)
I'd expect there to be a decent amount of VSCodium users as well, though.

[(deleted)]

withdrawn

[Michael Rothgang]

Any reasonable (to me) telemetry system allows opt-out, so will not report full numbers anyway.

[(deleted)]

Would collecting an aggregate count of Lean users, not broken down by platform or any other factor, be reasonable? This is all what I'm asking. This can be done server side, without adding tracking code to Lean.

[Bulhwi Cha]

Do we have to know the number of Lean users in the world?

[(deleted)]

Then I'm withdrawing my suggestion.

[(deleted)]

I do realize that tracking is sensitive. I suggested that we track the total user count because even Tails, an operating system for privacy sensitive people still keeps a count of total uses and uses this count to raise money for development. But it's clear there are members in this community that are against tracking in any form.

[Bulhwi Cha]

Conducting a survey could be an alternative to tracking users.

[Martin Dvořák]

Isn't it better to let Lean users self-identify as such?
https://leanprover-community.github.io/meet.html

[(deleted)]

People likely to take the survey are already active members of this Zulip. In fact the public discussions already provide enough insight into how Lean is used.

[Bulhwi Cha]

I think that's enough information we can get.