Website

Stream: general

[Bharat Bhat]

:rocket: Our new website is live!  :rocket:

Thanks to all who helped, especially @Corinna Calhoun @Sebastian Ullrich @Leonardo de Moura  :thank_you: :heart:

We hope you enjoy the new look & feel - we will continue to add to it in the coming weeks and months.

[Heather Macbeth]

Link: https://www.lean-lang.org/

[Bharat Bhat]

Should be the same link as always - thanks @Heather Macbeth !

[Floris van Doorn]

Looks very nice!

I noticed that https://lean-lang.org/lean4/doc/ (linked on the get started page) redirects to https://docs.lean-lang.org/lean4/doc which is a broken page (https://docs.lean-lang.org/lean4/doc/ - with the trailing slash - renders correctly)

[Asei Inoue]

We hope you enjoy the new look & feel - we will continue to add to it in the coming weeks and months

The impression was that the design of the website was not very sophisticated. I would have a more concrete opinion if the code was publicly available.

[Asei Inoue]

for example: in mobile, SNS icons displayed terrible...

image.png

[Asei Inoue]

There is a discomfort with the way the text is drawn together. I think it should not be centerd...

image.png

[Asei Inoue]

I think the icons should not be surrounded by a white square. Instead just using a different colour from the background is better, maybe

image.png

[Asei Inoue]

I find the text colour difficult to read. Wouldn't black be better?
Also, the face image should be bigger.
Difficult to tell the difference between the text being quoted and the text that represents the source of the quotation.

image.png

[Asei Inoue]

I would recommend hiring a web engineer and designer to fix these design problems...

[Mario Carneiro]

it looks like they hired one and that's why there is a new website

[Asei Inoue]

If he/she was already employed, then I would have said something bad about the person... I hope he/she will forgive me. I just want to make design cooler.

In my opinion, people (including me) would be more willing to contribute if the front-end code was made public, and that would improve the design considerably.

[Shreyas Srinivas]

1. The colour and font choice is unpleasantly reminiscent of the 2010s material design.
2. The resources section doesn't link to any resources, just news stories about lean (there's a separate learn page)
3. The download page links to lean3 downloads. I am afraid we are opening the doors to some chaos here

[Shreyas Srinivas]

4. The link in the downloads page to the community website seems to indicate that the community has some interest in lean3

[Shreyas Srinivas]

5. On a lighter note, on the resources page I learnt that @Kevin Buzzard 's mastodon link is grouped with a list of social media brand icons for official accounts (credits to Sabrina on discord): https://www.lean-lang.org/resources
   More seriously, I believe the links to prominent social media users of lean is a different category from social media icons of various platforms linking to official accounts of the organisation

[Shreyas Srinivas]

7. The buttons on this page sit beside the text. On mobile this results in large buttons vertically interleaved with the text and that can confuse users on their phones : https://www.lean-lang.org/community

[Mauricio Collares]

Whoa, great to see a friendlier website! Already found a couple of really interesting interviews I hadn't heard about before.

[Eric Wieser]

Shreyas Srinivas said:

I learnt that Kevin Buzzard 's mastodon link is grouped with a list of social media brand icons for official accounts

This does seem quite strange given how in the past people have mistakenly labelled Lean/mathlib as primarily Kevin's project!

[Eric Wieser]

Shreyas Srinivas said:

3. The download page links to lean3 downloads. I am afraid we are opening the doors to some chaos here

Linking directly to the binaries seems strange even for lean4; this is just setting users up for failure when they clone a package and don't have an elan installation to use the associated Lean version.

[Kevin Buzzard]

Eric Wieser said:

Shreyas Srinivas said:

I learnt that Kevin Buzzard 's mastodon link is grouped with a list of social media brand icons for official accounts

This does seem quite strange given how in the past people have mistakenly labelled Lean/mathlib as primarily Kevin's project!

I haven't used mastodon for a very long time either. I unfollowed everyone on X but still post stuff I think is ineresting. I'm not paying though, so I don't know who sees this stuff. But mastodon I don't use at all. I am surprised this link is there.

[Will Crichton]

I agree that the current design does not look particularly professional. I like some of the added colors and textures. Here's my brief attempt at what a fusion of the old and new designs could look like (figma link):
Screenshot 2024-09-28 at 9.25.04PM.png

[Asei Inoue]

I think old website was better…
please make frontend codes public..?

[Asei Inoue]

I can help to make website better

[Kim Morrison]

Thanks everyone for the feedback --- Corinna and Bharat are checking here and are seeing it! We're very happy to have suggestions and problems pointed out, and will iterate as appropriate. There's not really scope for anyone to assist beyond identifying problems, however.

[Shreyas Srinivas]

In that case, I'll add a point about aesthetics. The previous website gave the impression that we were looking at the theorem prover of the future. It was minimalistic, the font choice was elegant, and the content was immediately accessible, with no clutter. It did not convey the impression that lean was making a sales pitch for a startup product using a material design-like look from the last decade.

The current website has a lot of extraneous UI elements and is much more densely packed. It uncannily resembles the rust website. But the rust website feels cleaner, partly because of their spacing, colour, and lighter font choices and partly because they don't highlight the borders between page sections. Imho examples of good PL websites that are pleasing to the eye and convey content include the Haskell and Ocaml websites

[Asei Inoue]

@Shreyas Srinivas

The previous website gave the impression that we were looking at the theorem prover of the future. It was minimalistic, the font choice was elegant, and the content was immediately accessible, with no clutter. It did not convey the impression that lean was a mid 2010s startup trying hard to sell some bad enterprise product.

I agree! (edited)

[Shreyas Srinivas]

Enterprise product websites these days have also adopted designs with more spacing out of the elements and gentler fonts : https://www.cadence.com/en_US/home.html

[Shreyas Srinivas]

(deleted)

[Patrick Massot]

I don’t think there is any need to be so aggressive, and it won’t help.

[Shreyas Srinivas]

Oh no, that's not my intent.

[Shreyas Srinivas]

Apologies

[Shreyas Srinivas]

I'll tone it down to convey the point better

[Shreyas Srinivas]

The "Get Started" image appears blurry

[Shreyas Srinivas]

Uploading Screenshot_20240929-131418.png...

[Shreyas Srinivas]

Another point: colour choices are an important part of the lean brand. People instinctively associate colour with brands. At a PL conference, I only have to spot the yellow-orange stall to know that's Jane Street. In the PL context , the Auburn orange colour immediately reminds me of OCaml. Haskell has the purple-pink gradient on white with its familiar \lambda symbol. I spot the racket icon when I see the blue + red + white lambda. Python has the blue+yellow combo.

In summary, colours are integral to a brand identity. I would suggest choosing a nice colour palette for lean, because that will be around for a long time.

[Patrick Massot]

Shreyas Srinivas said:

Uploading Screenshot_20240929-131418.png...

You sent the message too quickly, before the upload was done. Yes, this is not the greatest Zulip feature…

[Shreyas Srinivas]

Screenshot_20240929-131418.png

[Shreyas Srinivas]

Thanks. It finally got uploaded

[Kim Morrison]

Shreyas Srinivas said:

I would suggest choosing a nice colour palette for lean

Done: #0073A3 and #000000 with accents of #F15732, as you see on the landing page. Enjoy. :-)

[Kim Morrison]

(I think some of the discussion above is wasting time. Pointing out links to the wrong things, accessibility issues, etc. are great.)

[Utensil Song]

Aesthetics aside, it's better if 3 keywords in "Why Lean?" are clickable, like the front page of https://www.roc-lang.org/ where 3 defining features of the language have links to dedicated pages to explain the "why", instead of just claiming so. Another style is https://odin-lang.org/ which has keyword links inside the one-paragraph explanation. Both styles will give newcomers a clear and professional impression. I'm particularly tempted to click "trust" to see why.

[Will Crichton]

Strong agree on the clickable links. Rust's website is another example, although it's a little colorful / noisy for my tastes: https://www.rust-lang.org/

[Patrick Massot]

I certainly tried clicking them.

[Jannis Limperg]

FYI, the "Resources > Publications" section is currently empty. The "Academic Citations" section has slightly confusing wording. Suggestion: "To cite Lean in an academic publication, please cite this paper [link]."

[Shreyas Srinivas]

Kim Morrison said:

Done: #0073A3 and #000000 with accents of #F15732, as you see on the landing page. Enjoy. :-)

This colour palette is not anywhere near ideal imho. The combination of colours doesn't seem to blend well at all.

[Shreyas Srinivas]

Also, the new landing page only mentions the functional programming aspect

[Shreyas Srinivas]

The words "verification" or "theorem prover" don't show up. But the news articles are all about math and theorem proving.

[Shreyas Srinivas]

Also I am not sure how well the colour palette holds up if and when the website has a dark mode

[Shreyas Srinivas]

The lines on the background graphic in the featured project section are also blurry.
Screenshot from 2024-09-29 14-26-30.png

[Shreyas Srinivas]

The orange font colour make the testimonials stressful on the eye to read.

[Asei Inoue]

@Kim Morrison

I think some of the discussion above is wasting time. Pointing out links to the wrong things, accessibility issues, etc. are great.

I'm sorry for being so noisy. But where is the line drawn for unproductive discussions?

Should we not point out problems from an aesthetic point of view on the website? For example, should we point out that the layout is broken when viewed from a mobile device?

[Ruben Van de Velde]

Being broken on mobile is not an aesthetic concern

[Shreyas Srinivas]

Screenshot_20240929-154945.png

The light blue background on part of the text is only found on the mobile version

[Jon Eugster]

I think on Desktop the website looks quite good already, modulo some minor details!

If you have the resources I do have 2 suggestions:

• I encourage you to look at the "Accessibility" feedback which the browser dev tools yield. For one thing, the text in orange is flagged as "bad contrast", which has been suggested here already. (and there are a few other minor suggestions)
• While Mathlib isn't a part of Lean in this sense, I think there is a sizable chunk of new people who do not know the difference. I think it would be desirable if the Get Started would mention this distinction a little bit better, so that an unknowing maths researcher certainly ends up with the correct installation instructions (maybe even linking to community's Get Started)

Screenshot_20240929_172434.png

[Corinna Calhoun]

Kevin Buzzard said:

Eric Wieser said:

Shreyas Srinivas said:

I learnt that Kevin Buzzard 's mastodon link is grouped with a list of social media brand icons for official accounts

This does seem quite strange given how in the past people have mistakenly labelled Lean/mathlib as primarily Kevin's project!

I haven't used mastodon for a very long time either. I unfollowed everyone on X but still post stuff I think is ineresting. I'm not paying though, so I don't know who sees this stuff. But mastodon I don't use at all. I am surprised this link is there.

Removed :)

[Corinna Calhoun]

Utensil Song said:

Aesthetics aside, it's better if 3 keywords in "Why Lean?" are clickable, like the front page of https://www.roc-lang.org/ where 3 defining features of the language have links to dedicated pages to explain the "why", instead of just claiming so. Another style is https://odin-lang.org/ which has keyword links inside the one-paragraph explanation. Both styles will give newcomers a clear and professional impression. I'm particularly tempted to click "trust" to see why.

Absolutely. We are working on developing clear information for these as well as the use cases.

[Shreyas Srinivas]

Shreyas Srinivas said:

Kim Morrison said:

Done: #0073A3 and #000000 with accents of #F15732, as you see on the landing page. Enjoy. :-)

This colour palette is not anywhere near ideal imho. The combination of colours doesn't seem to blend well at all.

The following is a well known website that suggests and explains choices of colour palette: https://coolors.co/

[Shreyas Srinivas]

and here is their take on the colour choices: https://coolors.co/contrast-checker/000000-0073a3
In particular for the orange text on white which has been described as stressful on the eye: https://coolors.co/contrast-checker/f15732-ffffff
This checker rates the contrast of text on background. There are other features which show good choices of colours

[Shreyas Srinivas]

It follows the web content accessibility guidelines: https://en.wikipedia.org/wiki/Web_Content_Accessibility_Guidelines

[Violeta Hernández]

Whoa, just opened the website again and it looks much nicer than it did a couple of days ago!

[Violeta Hernández]

I personally like the blue + orange accent combo, it's simple but yet not something I'd immediately associate to any other brand.

[Shreyas Srinivas]

Violeta Hernández said:

I personally like the blue + orange accent combo, it's simple but yet not something I'd immediately associate to any other brand.

Fedex? Granted it's slightly purple and not exactly blue.
Fanta?

[Deming Xu]

I think the new website having more images, icons, and dividers will ultimately be a good thing because it means that people are putting more effort into designing the site. I’ve also seen quite a few other websites use images of blurred, nearly white background blocks on the homepage to make the page less monotonous.

As for areas that need improvement, people have already mentioned that the web layout needs to adapt to mobile devices, not just laptops.

I’d like to add that I think a general principle is that maintaining consistency on a webpage is very important, which encompasses several of the issues people have raised before. It's like repeating a wrong sentence hundreds of times in different situations and it starts to sound like the truth. I find it interesting that consistency is more important than it seems. It makes the site appear far more symmetrical and serious.

In most places, we should use the same background color, rounded corner radius, shadows, spacing, and dividers. Font type, size, color, and alignment should be as uniform as possible. Try to use icons from the same icon library so that their style, complexity, and size remain consistent. Try to use vector graphics as much as possible instead of images.

(Especially, all blocks should either all have shadows or none; either all have rounded corners or none. From what I know, many large websites simply use the most common fonts, such as Arial, but I think using other fonts is also fine.)

In many cases, it is enough to just use black, white, and gray, along with varying opacities of a single primary theme color, like blue/green/yellow/purple. This is especially true for large color blocks like buttons.

If you need to break this rule of consistency and apply different styles to elements, you should have a reason for doing so. Perhaps the nature of the two elements is different, and they are not parallel, and you need to hint this to the user. Of course, I also think that for website prototypes, there is no need to care about any of these.

The text at the top of the page should be the shortest and most core content. As the user scrolls down, the text should gradually delve into more details.

For HTML, I think using Tailwind CSS for debugging is the most efficient way to go. You can directly modify class names and immediately see the improvements, instead of having to go through several steps like with native CSS. ChatGPT is actually also very good at writing decent small web pages using Tailwind.

Since someone mentioned accessibility, I’d like to say that I’m not sure why the fonts used on the Theorem Proving in Lean webpages are not black but instead a gray color like rgb(51,51,51). I always felt that my eyes got slightly more strained when reading this book. I think Functional Programming in Lean book uses the same website generator as TPIL, but its text is pure black.

[mars0i]

Most (not all) of the features listed on the old (current) "About" page are features that Agda and Idris have. But Lean is much better, I feel, so it's worth saying why, maybe even very explicitly: "Compared to other languages with these features, Lean excels because ...."

• Lean provides fast and informative interactive feedback. I'm not sure how to convey this succinctly in words, but having used Haskell, Agda, and Idris (and many other languages) before Lean, this might be what I love most. It's amazing. Maybe it's worth saying that you have to try it to truly appreciate it.
• Compared to Agda and Idris, tactics reduce the difficulties of dependently typed programming.
• Though not perfect, Lean has extensive documentation of functions, etc. (This should go without saying, but one can't take it for granted, as Agda shows.)
• Although Lean is still evolving, I gather that it's very solid, with a large user base. (This is an advantage over Idris. I suspect the user base is larger than Agda, too, but I don't know.)
• I haven't used Coq, but my sense is that Lean is easier to use.

Hygenic macros and metaprogramming seem like great features, and it's good that they're mentioned in the list of features, but I suspect most people would use these only occasionally at best. If that's right, then they are selling points, but not the most important ones.

[Niels Voss]

I wonder if its better to profess the advantages of Lean over other dependently typed languages, or the advantages of dependently typed languages over other languages. For the former, in addition to what mars0i said:

• Lean is the only major DTT language that has a massive centralized proof library, whose topics span more than just type theory and programming related topics (in particular, it has things like Calculus and Linear Algebra which are of general interest to mathematicians). My understanding is that in other languages, the proof libraries are nowhere near as unified, except maybe Isabelle's AFP.
• Lean has good support for classical reasoning, whereas most other proof assistants try to remain constructive as long as possible. I would ere on the side of caution about trying to make this a selling point though, because the people who know what classical vs constructive logic is are more likely to be the same people who want to work constructively. But maybe there's some point in trying to explain how Lean is mathematician-friendly, while at the same time not turning away anyone.
• Lean has good tooling (lake and elan) and good editor integration. If mentioning the VSCode plugin, maybe mention the Neovim and Emacs packages as well, just to avoid the impression of editor lock-in.

[Niels Voss]

For the code snipped on the website, would it be a good idea to have something that DTT languages can do but others can't? I feel like doing so would convey that Lean is fundamentally different from a language like Haskell, rather than just different in syntax. I was thinking of maybe a formalized bubble sort algorithm that is then proven correct, but I'm not sure that would fit in the box. There could potentially be multiple code snippets with arrows to cycle between them.