Discussion: New lean-lang.org

Stream: general

[Ashley Blacquiere]

Please use this thread to discuss the new lean-lang.org (see announcement here) Our immediate concern is with site stability, but we appreciate all feedback.

[Mario Carneiro]

The https://lean-lang.org/use-cases/mathlib/ site reads a bit LLMish, it's weird that this page has a conclusion section. It also should be linking to the actual website much more prominently

[Mario Carneiro]

in fact, I wonder if we can get the leanprover-community.github.io page bumped up to a blue button or header bar button somewhere here

[Dan Abramov]

IMO the absolute best learning resource is buried way down.

Screenshot 2025-07-06 at 19.14.15.png

Out of the first four, three would make me completely disengage and fall asleep. Speaking as a software developer with interest in math but who's not in academia.

Edit: To be more explicit, if you've never seen Lean, I think that the goal of this page is to get you to NNG, or at least to look at it. This is the thing that hooks you in. In that sense, the ordering on the old page gets it right.

[Mario Carneiro]

Mario Carneiro said:

in fact, I wonder if we can get the leanprover-community.github.io page bumped up to a blue button or header bar button somewhere here

more specifically, I think the community page link should be another box underneath zulip, and should not be under the "looking for more support?" header because it's not a support website

[suhr]

Maybe there should be a separation between learning material and the reference.

[Michael Rothgang]

Mario Carneiro said:

The https://lean-lang.org/use-cases/mathlib/ site reads a bit LLMish, it's weird that this page has a conclusion section. It also should be linking to the actual website much more prominently

The formatting of https://lean-lang.org/use-cases/flt/ also feels LLMish. The content itself is fine (the blurbs are a bit short on details, but still okay) - but short blurbs combined with the formatting scream "LLM" to me. It's probably untrue, but that is rather off-putting to me.

[Alan Moraes]

Links to Lean 4 (https://lean-lang.org/papers/lean4.pdf) and Lean 3 (https://lean-lang.org/papers/system.pdf) papers on https://lean-lang.org/learn/ are broken.

[Alan Moraes]

I'm also missing the publications page. Where is it located now?

[Ashley Blacquiere]

Alan Moraes said:

Links to Lean 4 (https://lean-lang.org/papers/lean4.pdf) and Lean 3 (https://lean-lang.org/papers/system.pdf) papers on https://lean-lang.org/learn/ are broken.

These links should now be fixed.

Alan Moraes said:

I'm also missing the publications page. Where is it located now?

We elected not to include a dedicated publications page. However, it's possible we'll reconsider this as we weigh out this and other content-related feedback above.

Thanks for all the comments so far - we're noting them all down!

[suhr]

Fancy cube you've got there: https://lean-lang.org/static/svg/cube.svg. There's one problem though: some labels jump instead of smoothly rotating with the cube. Looks a bit distracting.

[Aaron Liu]

woah

[Aaron Liu]

the website got a makeover

[Justin Asher]

This looks super slick!

[Justin Asher]

Michael Rothgang said:

The formatting of https://lean-lang.org/use-cases/flt/ also feels LLMish.

Probably want to enable mathjax here (e.g., for "if x, y, z, and n are positive integers with n ≥ 3, then x^n + y^n ≠ z^n").

[Michael Rothgang]

One detail that could already help: the outline on the right numbers every single subsection (no matter how short). If e.g. subsections were unnumbered, this would already remove some verbosity (which LLM output often has).

[Shreyas Srinivas]

On mobile, the height and position of the testimonials changes for each of them. This is jarring when one is scrolling on the mobile. I hope the size of the panel and the text positioning can be fixed. The deepmind testimonial has the best text positioning since the white coloured text doesn’t overlap with the white lines.

Otherwise, the website is great. The choice of blue feels much better this time.

[Joachim Breitner]

Thanks for the praise! I mean, pointing out issue is very useful, but pointing out what’s good feels very good, especially for those who worked laboriously on the new website release.

[Shreyas Srinivas]

I also like how the colour and accents work well in both light and dark mode. The font selection is good and the graphics blend well enough and are non-intrusive (which is a huge positive).

One little content quibble. For the citations, it might be more useful to provide standard citation texts instead of linking to the pdf. Like bibtex.

[Arthur Adjedj]

The main page refers to Lean as both a theorem prover and a programming language, but both of the examples shown on the side ("Powerful automation" and "Mathematics") advertise the proving capabilities of the language. Perhaps this part could benefit from having one or two "programming" examples, potentially showing the extensibility of the language.

[Mario Carneiro]

Overall I think the website is much improved, both compared to old version and also the last redesign attempt. Big thanks to everyone who worked on it :+1:

[Alex Kontorovich]

Love it already!! :)
image.png

[Ayhon]

Agreed, I liked the previous version of the website, but this new one is definitely an improvement!

[Ayhon]

Maybe Verso could adopt a similar UI design? :eyes:

[Winston Yin (尹維晨)]

Love the new design: colours, subtle animation, etc! A super minor stylistic point. At least on mobile, the text slightly fades as you go from top to middle of the screen. That seems a little counterintuitive to me, as I would expect to read clearer, darker text over much of the page, rather than only near the top banner. Perhaps the fading was meant to occur much lower on the screen?

[Oliver Dressler]

The new design is great! Im accessing on mobile and it works well. Its great that the page is full of calls to action! Focus on getting started (install) and practical examples on the landing page are great. Enjoying the subtle blue gradients. Overall a big improvement!

Minor things:

• The text font on the lean FRO Home page has a different color, more blue, less contrast. I think at least the bold parts should be more black like on other pages.
• I would prefer the LEAN logo (home link) top left to be classic black instead of blue. But I understand the decision. In dark mode, blue works fine.
• Some organisations randomly shuffle the order of members on each page access. Both ways have advantages, just some food for thought.

[Niels Voss]

I really like this new design! One comment I have is that I think maybe the choice of the first code example should be reconsidered. When I learned Lean, I didn't even know what a formal proof was and I certainly didn't know what a tactic was. So I think saying that saying that grind goes "beyond standard tactics" is not very helpful. In my opinion, the impression it gives off right now is that Lean is a type of CAS.

[Niels Voss]

If this was intended for programmers, I would rather have an example of something like showing how Lean can do safe array indexing or by proving indices are within bounds or validate an algorithm like bubblesort, which are things you can't do in other languages but which programmers might like to do

[Shreyas Srinivas]

Oliver Dressler said:

• I would prefer the LEAN logo (home link) top left to be classic black instead of blue. But I understand the decision. In dark mode, blue works fine.

The current design is more consistent with the ambient colour context. Also the same colour works for both dark and bright mode. So I prefer the current colour

[metakuntyyy]

Dan Abramov said:

IMO the absolute best learning resource is buried way down.

Screenshot 2025-07-06 at 19.14.15.png

Out of the first four, three would make me completely disengage and fall asleep. Speaking as a software developer with interest in math but who's not in academia.

Edit: To be more explicit, if you've never seen Lean, I think that the goal of this page is to get you to NNG, or at least to look at it. This is the thing that hooks you in. In that sense, the ordering on the old page gets it right.

Seriously, we need way more games working out of the box in the browser like the natural numbers game.

[Riccardo Brasca]

Isn't the example

example (x : Nat) : 0 < match x with
  | 0   => 1
  | n+1 => x + n := by
  grind

a little cryptic to be shown in the homepage? (My mathematician's mind was completely confused by it, but maybe for programmers is completely fine.)

[Shreyas Srinivas]

programmers are not accustomed to writing match statements in the lhs of a definition either. This stuff only works in dependently typed languages and those are really not common.

[Jz Pan]

/-- The factorial is non-negative -/
theorem factorial_non_negative : ∀ n, 0 < n ! := by

The theorem name and docstring don't match with its formal statement.

[Joachim Breitner]

Ah, my bad, confusing nonnegative and positive in the late evening. Thanks!

[Marcus Rossel]

Riccardo Brasca said:

My mathematician mind was completely confused by it

My CS mind thought it was a typo first

[suhr]

A less cursed formatting would help:

example (x: Nat): 0 < (match x with | 0 => 1 | n+1 => x + n) := by
  grind

But moving match into a separate definition would still be better.

[Mario Carneiro]

I know grind is new and shiny but I'm not sure it's the best option for a first code example. Maybe something a little more like hello world? Define fibonacci, eval it at 17, prove it is everywhere positive

[Mario Carneiro]

It's also being used in almost every proof in the second code example. I think we should probably forestall the impression that lean only has one tactic

[suhr]

Mario Carneiro said:

I think we should probably forestall the impression that lean only has one tactic

Well, Isabelle/HOL also has only two tactics: one is auto and the other one is hammer.

[suhr]

Jokes aside, it's hard to show apply?, rw? and dsimp in a polished proof example. But maybe one should avoid grind where a humble simp is sufficient.

[Kevin Buzzard]

Mario Carneiro said:

I know grind is new and shiny but I'm not sure it's the best option for a first code example. Maybe something a little more like hello world? Define fibonacci, eval it at 17, prove it is everywhere positive

nonnegative ;-)

[Mario Carneiro]

ah, that's annoying

[Mario Carneiro]

maybe factorial instead

[Mario Carneiro]

(the intention of the example is to show three things:

• Definition by recursion
• Lean can be used like a CAS / python, and it has an unbounded number type
• Lean can be used to prove theorems that can't be established by checking every input

)

[suhr]

• Lean can automatically prove theorems that can be established by checking finite number of inputs

[suhr]

by decide deserves a bit of love I think.

[Mario Carneiro]

I'm not sure it will be easy to do that in a 15 line code example. The issue is that at this point readers won't know the difference between proofs on infinite domains and finite, it's all just "lean does magic and then theorem is proved"

[Mario Carneiro]

I think you need to have at least a short comment before a by decide proof which says that it works by trying all the inputs

[Mario Carneiro]

I looked around for what other languages do.

Go:

package main

import "fmt"

func main() {
    fmt.Println("Hello, 世界")
}

[Mario Carneiro]

Haskell:

primes = filterPrime [2..] where
  filterPrime (p:xs) =
    p : filterPrime [x | x <- xs, x `mod` p /= 0]

[Mario Carneiro]

Scala:

val fruits =
  List("apple", "banana", "avocado", "papaya")

val countsToFruits = // count how many 'a' in each fruit
  fruits.groupBy(fruit => fruit.count(_ == 'a'))

for (count, fruits) <- countsToFruits do
  println(s"with 'a' × $count = $fruits")
// prints: with 'a' × 1 = List(apple)
// prints: with 'a' × 2 = List(avocado)
// prints: with 'a' × 3 = List(banana, papaya)

[Mario Carneiro]

Rocq:

From Stdlib Require Import Lia.

Fixpoint fac n :=
  match n with
  | 0 => 1
  | S n' => n * fac n'
  end.

Compute fac 5.

Lemma fac_succ n : fac (S n) = S n * fac n.
Proof. reflexivity. Qed.

Lemma fac_pos n : fac n > 0.
Proof.
  induction n.
  - simpl. lia.
  - rewrite fac_succ. lia.
Qed.

From Corelib Require Import Extraction.
Extraction Language OCaml.
Extraction fac.

[Mario Carneiro]

dammit rocq literally did factorial, compute and positive

[Mario Carneiro]

The new rocq webpage is pretty nice though: https://rocq-prover.org/ They redesigned it this year along with the name change

[Mario Carneiro]

fac_succ is a nice addition to the example, it shows that definitional equality is a thing

[Mario Carneiro]

the last bit about code extraction is unfortunately not so easy to demo in lean

[Matthew Ballard]

The new website looks great! I first perused it on (tiny) mobile and found it much more friendly than the old one.

One request: could the toggle for light/dark mode detect the system or browser settings and mirror that automatically?

[Matthew Ballard]

Mario Carneiro said:

The new rocq webpage is pretty nice though: https://rocq-prover.org/ They redesigned it this year along with the name change

It does look very nice. In particular, I like the
trusted and awards blurbs. I do imagine that something could be generated for Lean that would be quite impressive.

On the other hand, the new Rocq page is a bit crowded even on a giant screen. So I understand the desire to strongly gate content on the landing page.

[Mario Carneiro]

The overall font size of the lean website is pretty big, it looks about 80% larger than the rocq website

[Mario Carneiro]

I think it could be turned down about 30% and still be quite big and clear

[Shreyas Srinivas]

@Henrik Böving mentioned on discord a few months ago that the design comes from that of the OCaml website

[Shreyas Srinivas]

I disagree about the font size. Big font sizes are good for accessibility reasons as well as keeping the text short and well-highlighted.

[Henrik Böving]

Shreyas Srinivas said:

Henrik Böving mentioned on discord a few months ago that the design comes from that of the OCaml website

https://github.com/rocq-prover/rocq-prover.org?tab=readme-ov-file#acknowledgments it's quite literally a fork yeah, https://ocaml.org/

[Shreyas Srinivas]

The Ocaml website has even bigger font sizes

[Mario Carneiro]

Shreyas Srinivas said:

I disagree about the font size. Big font sizes are good for accessibility reasons as well as keeping the text short and well-highlighted.

Sure, no disagreement here. But there's big and then there is "logo takes up 100% of the space of a large monitor full screen"

[Mario Carneiro]

looking at other major sites like https://react.dev/, https://code.visualstudio.com/, https://nodejs.org/en, it seems like lean's header is about 40-50% larger than average

[Mario Carneiro]

The react website body text font size looks good to me. It's still almost double the size of the body text on this chat, and it has single paragraphs + images taking up screenfulls at a time, but there is room to write two paragraphs in a side by side example, which is good for if you want to have a showcase similar to what the rocq website is doing

[Mario Carneiro]

I was wondering if https://www.apple.com/ does differently since they love to emphasize design but their text is tiny!

[Matthew Ballard]

https://www.swift.org

[Matthew Ballard]

Picking at nits and being terribly parochial but with the
bullet properties I think nouns would be more punchy. Eg: Trustworthy => Trust.

Powerful => Power would be more punchy but it seems the emphasis there is on productivity or simplicity (relatively) more so. Extensible => _ ... I cannot think of a better one

[Matthew Ballard]

"Trust, Tooling, Tailorability" would be smooth

[Matthew Ballard]

If you want verbs:

• "Believe, Achieve, Evolve"
• "Solidify, Amplify, Diversify"
• "Trust, Build, Grow"

[Shreyas Srinivas]

Matthew Ballard said:

If you want verbs:

• "Believe, Achieve, Evolve"
• "Solidify, Amplify, Diversify"
• "Trust, Build, Grow"

All these sound like generic marketing jargon on an advertisement.

[Mario Carneiro]

Matthew Ballard said:

Extensible => _ ... I cannot think of a better one

Extensibility?

[Matthew Ballard]

It says some version of "extends" three times at the moment in limited space.

To be clear, I am just riffing here in between commitments.

[Mario Carneiro]

the swift webpage is pretty snazzy

[Mario Carneiro]

I like the color contrasts

[Matthew Ballard]

If I look at swift then I am obliged to look at https://go.dev and https://www.rust-lang.org. The former has alliteration and the latter has nouns.

[Wrenna Robson]

Mario Carneiro said:

The https://lean-lang.org/use-cases/mathlib/ site reads a bit LLMish, it's weird that this page has a conclusion section. It also should be linking to the actual website much more prominently

I want to echo this - it really reads VERY much like it was written by an LLM. In particularly the em-dash usage stands out a little, but also the whole structure. I realise the degree of AI scepticism will vary across the Lean community but I personally find most AI generated prose quite unpleasant to read, and I'm sorry to say I somewhat feel this has that vibe to it.

[Wrenna Robson]

Love the general design though.

[Wrenna Robson]

Not massively convinced by the usefulness of Resivoir but time will tell (it is hard to tell which packages are up to date or are useful - there's not much in the way of quality measures).

[Henrik Böving]

Just FYI, reservoir has existed for basically a year by now, this is only a redesign of the web UI

[Wrenna Robson]

Most importantly: who is this cute little fella?

[Wrenna Robson]

image.png

[Wrenna Robson]

Do they have a name? Can I buy a plushie?

[Michael Rothgang]

crates.io in Rust is massively helpful --- so this reservoir manages to come close, it will have been worth it!

[Wrenna Robson]

Oh I think it seems like the right thing to have - I was just struck by the fact that e.g. I search crypto and I got a real mixed bag of results.

[Wrenna Robson]

BUT I found a project I was not aware of that is using a FCF-like methodology in Lean - very cool.

[Wrenna Robson]

Wrenna Robson said:

Do they have a name? Can I buy a plushie?

(In seriousness - I would buy some Lean merch, just saying.)

[Joscha Mennicken]

The blue tone of the main page and reservoir differ ever so slightly.

[Joscha Mennicken]

Another tiny nitpick: The corners of the logo in the footer are a bit broken (which is visible at default resolution on high-dpi displays):
image.png

[Kevin Buzzard]

Aah this brings me back to the old days (2018?) where the L and the E in the logo on the web page didn't quite join together perfectly :-)

[Weiyi Wang]

There should be a formalization of Lean logo coordinates

[Mauricio Collares]

Kevin Buzzard said:

Aah this brings me back to the old days (2018?) where the L and the E in the logo on the web page didn't quite join together perfectly :-)

2021! #general > logo @ 💬

[Sofia Rodrigues]

Joscha Mennicken said:

Another tiny nitpick: The corners of the logo in the footer are a bit broken (which is visible at default resolution on high-dpi displays):
image.png

Fixed :)

[Sofia Rodrigues]

Joscha Mennicken said:

The blue tone of the main page and reservoir differ ever so slightly.

That's intentional

[Joscha Mennicken]

Sofia Rodrigues said:

Joscha Mennicken said:

Another tiny nitpick: The corners of the logo in the footer are a bit broken (which is visible at default resolution on high-dpi displays):
image.png

Fixed :)

Now only the LEAN logo on the Reservoir footer is still broken :P

[Sofia Rodrigues]

Wrenna Robson said:

Do they have a name? Can I buy a plushie?

I’m planning to draw more illustrations of this hexapus in the future (so I can try to convince David to add some cute drawings to the books just like Rust does with Ferris :P). but they don’t have a name yet.

[Wrenna Robson]

Could I suggest "Nael"?

[Wrenna Robson]

(Lean backwards, natch!)

[Miyahara Kō]

< I won't give up my spot as the Lean mascot to anyone

[Mario Carneiro]

Wrenna Robson said:

Could I suggest "Nael"?

I have to admit I've seen the lean logo in various orientations on laptop stickers and such, and given the fact that two of the 4 letters are upside down and one of them is rotationally symmetric, it's actually easier to read it as NAEL than as LEAN

[Wrenna Robson]

To me, further evidence that this is the true name of our six-limbed friend.

[Wrenna Robson]

rustacean :: cephaleanopod?

[Anthony Fernandes]

First: amazing upgrade of the website, very clean and beautifully designed. Now just a small thing: there are HTML tags hanging around in the 3rd step of the install process
image.png

[Dan Abramov]

I'm noticing there's quite a few old links in Google results that don't have any appropriate redirects.

For example, https://lean-lang.org/documentation/widgets/

I'm pretty sure I also saw it for reference documentation pages though I don't remember which ones.

Screenshot 2025-07-08 at 17.27.12.png
Screenshot 2025-07-08 at 17.27.16.png

It might be a good idea to set up a few redirect patterns if there is any common pattern. E.g. if some material just moved the root routes. Not sure if those downright don't exist anymore.

In particular it feels very disorienting when googling things.

Edit: Maybe it's worth looking at top 404 logs if there are any access logs. Or via Google Search Console if it's set up.

[Dan Abramov]

Is the website open source? I can't find the repo. I wanted to send a proposed change to move "Interactive Games and Tutorials" above "Further Reading". (NNG is brilliant and IMO deserves a prime spot, there's no way someone should look at this page and be able to miss it exists.)

But I couldn't find where to make the change.

[Joscha Mennicken]

Wrenna Robson said:

rustacean :: cephaleanopod?

Coleoidea are apparently a subclass of cephalopoda, and isn't Lean also kind of a Leo idea?

[Matthew Ballard]

Something I noticed on iPadOS 26 was the extra space at certain aspect ratios.

[Matthew Ballard]

Another iteration: Trust, Types, Tooling.

[Sofia Rodrigues]

Dan Abramov said:

Is the website open source? I can't find the repo. I wanted to send a proposed change to move "Interactive Games and Tutorials" above "Further Reading". (NNG is brilliant and IMO deserves a prime spot, there's no way someone should look at this page and be able to miss it exists.)

But I couldn't find where to make the change.

It's not open source yet. but I'm going to change that :) I also think NNG deserves to be highlighted.

[(deleted)]

The Natural Number Game must be at the very top of the page. As other members said, this is the single most helpful resource for starting out.

[(deleted)]

How to cite Lean should be an entirely separate page

[(deleted)]

I agree that the 3 pages for the 3 Lean projects look very boring as they are LLM generated. Maybe linking directly to their GitHub repositories from the start is a better idea :eyes:

[(deleted)]

The site looks quite nice I like it

[Justin Asher]

Sofia Rodrigues said:

It's not open source yet. but I'm going to change that :)

Would be happy to submit some PRs if this happens!

[Sofia Rodrigues]

Justin Asher said:

Sofia Rodrigues said:

It's not open source yet. but I'm going to change that :)

Would be happy to submit some PRs if this happens!

I didn’t phrase that right. It’s not my choice to make it public, I just meant I’m going to put NNG in a better spot on the page.

[Patrick Massot]

Sofia, NNG is indeed great, but note that people with different backgrounds have different favorite entry points. Non-mathematicians users are especially enthusiastic about NNG, but they are not all users.

[Alok Singh]

Patrick Massot said:

Sofia, NNG is indeed great, but note that people with different backgrounds have different favorite entry points. Non-mathematicians users are especially enthusiastic about NNG, but they are not all users.

But I think the enthusiasm NNG elicits is rather unique for it. I can't think of another Lean project with the same fun buy-in. Even mathematicians have something to like about it because it gives an intro to Lean.

[Yaël Dillies]

I would think mathematicians quite enjoy NNG, actually? I was certainly enthused

[Kevin Buzzard]

Definitely some but not all enjoy it!

[Joscha Mennicken]

It would be nice if this link for subscribing to the office hours calendar via iCal was somewhere near the calendar on https://lean-lang.org/community/.

[Willem vanhulle]

I briefly looked at the manual installation instructions and Mathlib updates. I am still a bit puzzeled about how to properly use lake subcommands for maintaining a real world Lean library / binary. Things like updating dependencies versus updating toolchain in a project could be better explained.

[Willem vanhulle]

Another remark: font in tooltips for tactics above Lean code in the mobile iOS Safari version are unreadable because text inside overflows horizontally and is cut off.

[Willem vanhulle]

In the footer a documentation section with links is mentioned next to a section resources with links. However, for me “loogle” is definitely documentation and should be under documentation. The section “resources” feels a bit disorienting for me. Maybe restrict the section to well know Lean software libraries?

[Ashley Blacquiere]

Thanks for the feedback, @Willem vanhulle.

And just a broad FYI: We continue to monitor this thread and take all feedback into account. We won't likely respond directly to any one particular comment, but we are tracking and considering it all. And some of the earlier feedback in this thread has already been addressed. Thanks all.

[Joscha Mennicken]

The URLs for the road maps contain the substring 1900-1-1, which looks like a date. For example: https://lean-lang.org/fro/roadmap/1900-1-1-the-lean-fro-year-3-roadmap/

This doesn't add any information to the URL, but only makes it longer. Maybe it's a configuration mistake somewhere? If you do decide to change the URLs, redirects for the old ones would be nice.

[Kim Morrison]

I suspect this is an artifact of these page being written in "blog mode", but without a date field specified in the sources.

[Eric Wieser]

Congratulations on over 125 years of Lean!

[Bolton Bailey]

It seems the "use cases" link on https://live.lean-lang.org/ is broken

[Shreyas Srinivas]

The url in the live editor is /usecases. The correct one is /use-cases. The ideal solution for this issue and the space issue for the live editor mentioned in the other thread is to remove it there