Home Page

Stream: general

[Cole Shepherd]

The Lean homepage (leanprover.github.io) currently states Lean is a theorem prover. This will put off people looking for a general purpose programming language. Can we please update this to say something like "programming language and theorem prover"?

image.png

[Alex J. Best]

Well if someone clicks the "about" link they get told "Lean is a functional programming language", so while theres a change someone could leave right after the landing page I'm not sure we need to worry too much about people being confused if they read beyond the introduction. Also the page you link to is actually an image so I imagine its nontrivial to change, so I wouldn't bet on microsoft research changing it so often.

[Cole Shepherd]

True. I'd argue the "About" page should actually be the home page. The home page as it stands now is useless, though it looks nice.

[Eric Wieser]

Note that only a vanishingly small number of people on this Zulip instance have the power to make decisions about the home page of leanprover.github.io. The site maintained by the community at https://leanprover-community.github.io/ is easier to change.

[Eric Wieser]

The source code for that page is here

[Kind Bubble]

Eric Wieser said:

Note that only a vanishingly small number of people on this Zulip instance have the power to make decisions about the home page of leanprover.github.io. The site maintained by the community at https://leanprover-community.github.io/ is easier to change.

Oh, since you mention that, do you know who administrates this Zulip instance?

[Mario Carneiro]

https://leanprover.zulipchat.com/#organization/user-list-admin