What is the best computer configuration for writing Lean?

Stream: new members

[张守信(Shouxin Zhang)]

Hi everyone,

As we all know, having Lean 4 provide responsive feedback in the infoview is crucial for a smooth proving workflow. Similarly, when using tactics like rw?, apply?, or simp?, we ideally want quick suggestions (though realistically, this can often take several seconds or more). When the system feels sluggish, it can be quite frustrating and impact productivity. I often find myself wishing for a faster setup.

This leads me to my main question: What is currently considered a good or even optimal computer configuration for working effectively with Lean 4?

I'm curious about recommendations for both desktops and laptops. For instance, while desktops often have superior GPU performance for gaming, my understanding is that Lean primarily relies on the CPU. Is that correct?

Specifically, what kind of specs should one look for regarding:

• CPU: (Clock speed? Core count?)
• RAM: (How much is recommended for a smooth experience, especially with large projects like Mathlib? 16GB? 32GB? More?)
• Storage: (Is a fast SSD, like NVMe, significantly beneficial? What capacity is comfortable?)
• GPU: (Is it largely irrelevant for Lean performance?)

Also, does Lean 4's performance or the overall development experience differ noticeably between operating systems, such as macOS versus Windows (perhaps using WSL)?

Essentially, if one wanted to configure a system (within a reasonable budget for a standard PC/laptop) to minimize waiting times and maximize responsiveness when writing Lean code, what would you advise?

Thanks in advance for any insights or recommendations!

[Henrik Böving]

There's been a couple of threads about this recently like #general > Recommend me a PC under 2000 € #general > Mathlib as a PC benchmark #general > new (mac) laptop for Lean. The bottom line is:

• CPU is mostly more is better given that Lean is a very CPU intensive and parallel application. The Apple hardware is pretty good, the recent AMD chips are also pretty good, don't know about intel.
• RAM at least 16 though 32 doesn't hurt (that said you can in theory at least compile mathlib on an 8 GB machine if you really want to)
• A full mathlib checkout with cached build artefacts is ~11 GB so you might even be able to just get away with 256 GB if you don't have much other stuff? Though with how cheap storage is nowadays I don't really see a reason not to spec for 512GB or 1TB (or more depending on what you want to do)
• GPU doesn't matter at all

Afaik we have established by now that running Lean on macos and Linux is going to be notably faster than on Windows, dunno about WSL.

[张守信(Shouxin Zhang)]

Henrik Böving said:

There's been a couple of threads about this recently like #general > Recommend me a PC under 2000 € #general > Mathlib as a PC benchmark #general > new (mac) laptop for Lean. The bottom line is:

• CPU is mostly more is better given that Lean is a very CPU intensive and parallel application. The Apple hardware is pretty good, the recent AMD chips are also pretty good, don't know about intel.
• RAM at least 16 though 32 doesn't hurt (that said you can in theory at least compile mathlib on an 8 GB machine if you really want to)
• A full mathlib checkout with cached build artefacts is ~11 GB so you might even be able to just get away with 256 GB if you don't have much other stuff? Though with how cheap storage is nowadays I don't really see a reason not to spec for 512GB or 1TB (or more depending on what you want to do)
• GPU doesn't matter at all

Afaik we have established by now that running Lean on macos and Linux is going to be notably faster than on Windows, dunno about WSL.

Thank you for your response! Assuming I must use the Windows operating system for general-purpose use, I'd like to know which CPU offers better performance: the U9-285K or the R9-9950X? It's said that the U9 has stronger single-core performance, so I'm wondering if it would compile a single Lean file faster than the R9?

Also, how does the speed of an R9-9950X on a Windows host running Linux via WSL compare to a Mac laptop with an M4 Max chip? (This is also important! Because we can always expect good things from Mac CPUs.)