desktop processors for using lean and other proof assistants

Stream: general

[Bulhwi Cha]

Do you think the Intel Core i7-9700 processor will remain powerful enough for building and testing Lean projects? I've used it for five years, and I'm planning to upgrade it in two or three years.

[Gavin Zhao]

Your current CPU's 3.0GHz base frequency is good enough. If you often build super large projects (like mathlib) from scratch, you might need more cores/threads, but for most purposes 8 threads is enough.

[Gavin Zhao]

I've found that RAM size is much more important to me than my CPU. You're much more likely to be limited by Lean files that take up several GB of RAM each when opened. You should monitor your RAM usage to see the files that you typically open and check if you need to upgrade the RAM.

[Gavin Zhao]

(my usecase requires me to have multiple files opened side-by-side, and each file I open in Lean InfoView sits there in RAM even after I close the file in my editor unless, uh, I don't even know how to tell the Lean LSP to drop it)

[Bulhwi Cha]

One of my Lean files imports Mathlib.Data.Set.Basic and contains two theorems I wrote. It takes up 861 MiB of RAM. Can someone explain the reason for this? I'm just curious.

My Lean file

-- this code is written in Lean v4.26.0

module

public import Mathlib.Data.Set.Basic

namespace Set

open Function

universe u

theorem ext' {α : Type u} {A B : Set α} (h : ∃ (f : A → B), Surjective f ∧
    ∀ (a : A), ∃ (haB : a.val ∈ B), f a = ⟨a.val, haB⟩) : A = B := by
  let ⟨f, hsur, heq⟩ := h
  ext
  constructor
  · next x =>
    intro hxA
    let ⟨(hxB : x ∈ B), (hfx : f ⟨x, hxA⟩ = ⟨x, hxB⟩)⟩ := heq ⟨x, hxA⟩
    exact hxB
  · next y =>
    intro hyB
    let ⟨⟨x, hxA⟩, hfa₁⟩ := hsur ⟨y, hyB⟩
    let ⟨(hxB : x ∈ B), (hfa₂ : f ⟨x, hxA⟩ = ⟨x, hxB⟩)⟩ := heq ⟨x, hxA⟩
    have : x = y := by
      refine Subtype.mk.inj (show ⟨x, hxB⟩ = (⟨y, hyB⟩ : B) from ?_)
      rw [← hfa₁, hfa₂]
    subst y
    exact hxA

theorem ext_iff' {α : Type u} {A B : Set α} : A = B ↔ ∃ (f : A → B), Surjective f ∧
    ∀ (x : A), ∃ (hxB : x.val ∈ B), f x = ⟨x, hxB⟩ := by
  constructor
  · intro h
    exists fun x ↦ ⟨x.val, h ▸ x.property⟩
    constructor
    · intro y
      exists ⟨y.val, h.symm ▸ y.property⟩
    · intro x
      exists (h ▸ x.property)
  · exact ext'

end Set

[Michael Rothgang]

Data point: in October, I learned that 8 GB of RAM were not enough to reliably do import Mathlib in a project depending on mathlib without making your computer run out of memory. The module system and other fixes have helped somewhat (resp. will, if your project also uses the module system) --- but I wouldn't base my RAM choices on this. Go for at least 16GB of RAM, and even better 32 if you easily can.

[Gavin Zhao]

Bulhwi Cha said:

One of my Lean files imports Mathlib.Data.Set.Basic and contains two theorems I wrote. It takes up 861 MiB of RAM. Can someone explain the reason for this? I'm just curious.

My Lean file

-- this code is written in Lean v4.26.0

module

public import Mathlib.Data.Set.Basic

namespace Set

open Function

universe u

theorem ext' {α : Type u} {A B : Set α} (h : ∃ (f : A → B), Surjective f ∧
    ∀ (a : A), ∃ (haB : a.val ∈ B), f a = ⟨a.val, haB⟩) : A = B := by
  let ⟨f, hsur, heq⟩ := h
  ext
  constructor
  · next x =>
    intro hxA
    let ⟨(hxB : x ∈ B), (hfx : f ⟨x, hxA⟩ = ⟨x, hxB⟩)⟩ := heq ⟨x, hxA⟩
    exact hxB
  · next y =>
    intro hyB
    let ⟨⟨x, hxA⟩, hfa₁⟩ := hsur ⟨y, hyB⟩
    let ⟨(hxB : x ∈ B), (hfa₂ : f ⟨x, hxA⟩ = ⟨x, hxB⟩)⟩ := heq ⟨x, hxA⟩
    have : x = y := by
      refine Subtype.mk.inj (show ⟨x, hxB⟩ = (⟨y, hyB⟩ : B) from ?_)
      rw [← hfa₁, hfa₂]
    subst y
    exact hxA

theorem ext_iff' {α : Type u} {A B : Set α} : A = B ↔ ∃ (f : A → B), Surjective f ∧
    ∀ (x : A), ∃ (hxB : x.val ∈ B), f x = ⟨x, hxB⟩ := by
  constructor
  · intro h
    exists fun x ↦ ⟨x.val, h ▸ x.property⟩
    constructor
    · intro y
      exists ⟨y.val, h.symm ▸ y.property⟩
    · intro x
      exists (h ▸ x.property)
  · exact ext'

end Set

My guess is that Lean LSP has loaded Prelude + all the transitive imports of Mathlib.Data.Set.Basic into RAM...

[Gavin Zhao]

Go for at least 16GB of RAM, and even better 32 if you easily can.

An unfortunate time to buy new RAM :sweat_smile:

[Bulhwi Cha]

I have a pair of 16 GB DDR4 RAM, and I guess I'll have to use it for the next few years. I was only able to upgrade my graphics card. :smiling_face_with_tear:

[Bulhwi Cha]

Does Lean require more memory than other proof assistants like Rocq, Agda, Isabelle, and Metamath One?

[Martin Dvořák]

Gavin Zhao said:

I've found that RAM size is much more important to me than my CPU. You're much more likely to be limited by Lean files that take up several GB of RAM each when opened. You should monitor your RAM usage to see the files that you typically open and check if you need to upgrade the RAM.

Yes, but at a certain point, more RAM will not help, whereäs faster CPU will continuously help.