Lean is slow?

Stream: general

[Patrick Massot]

I really wonder where he heard complaints about Lean’s performance.

[Shreyas Srinivas]

We still get a lot of these complains on Zulip, although this is usually because people have strange setups or antivirus/firewall issues. That being said lean is much faster now than it was in July 2024.

[Kevin Buzzard]

I read a lot of zulip and I don't see people complaining that lean is slow except in the context of "this is slow" "aah but do it that way" "oh now it's fast". The Jacobi-Zariski file in mathlib is an exception but even that gets faster over time (and if people stopped believing in universes then it would get even faster) (and there's also no evidence that if they managed to get that far in algebra in Isabelle then it wouldn't be slow there too, or even that it's even possible to get that far in algebra in Isabelle).

However Larry has access to sledgehammer which I think is really the big win for simple type theory.

[Alex Meiburg]

I don't see people complaining that lean is slow except ...

As I've recently come to realize, this is really what exactly what 'slow' often means. For instance, Python is 'slow', but of course people write performant code in Python all the time. (Sometimes this means using numpy effectively, sometimes it means avoiding dynamic dispatch...) The same goes for Julia (my other less-standard favorite language beside Lean), which is typically advertised as being "as fast as C", but if you're not careful you really can end up in slow code again. Basically any garbage collected language has pitfalls about re-allocating many objects, too.

I think this can be true for Lean, too

[Andrew Yang]

I totally agree that lean often forces us to do (otherwise) suboptimal or unintuitive approaches just because of bad performance. The only reason why they aren't complained a lot on Zulip is just that complaining doesn't really solve the problem and there are well know workarounds like defining auxiliary types to stop lean from unfolding stuff or hand tweaking priorities of instances, but the fact that lean is forcing me to do this is still suboptimal and a symptom of lean being slow. (Of course I am not saying that lean could do better or that other proof systems would be faster)

More concretely, here's an example that should just work but doesn't that I just encountered last week. These things aren't that uncommon.

import Mathlib

open TensorProduct

variable {R R' S : Type*} (R'' : Type*) [CommRing R] [CommRing R'] [CommRing R''] [CommRing S]
    [Algebra R R'] [Algebra R' R''] [Algebra R R''] [IsScalarTower R R' R''] [Algebra R S] (e : R' ⊗[R] S)

#synth IsScalarTower R R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}))

[Bhavik Mehta]

I think it's also fairly easy to run into situations where Lean appears really slow, eg the server taking a surprisingly long time to respond with feedback. Here's a quick example I just recorded, where after typing simp on a very simple goal, I have to wait ten seconds before I get any updates from Lean.
Screen Recording 2025-11-02 at 21.48.24.mov
In situations like this, I think it's not surprising for a (especially new) user to think "Lean is slow", and not complain because it just seems par for the course.

[James E Hanson]

Kevin Buzzard said:

(and there's also no evidence that if they managed to get that far in algebra in Isabelle then it wouldn't be slow there too, or even that it's even possible to get that far in algebra in Isabelle).

Kevin, I feel like you're not justified in just asserting that there is "no evidence" that it would be possible to formalize Jacobi-Zariski in Isabelle.

[Ruben Van de Velde]

Only in the sense that it hasn't happened yet, I imagine

[pandaman]

people have regularly asked why Isabelle dispenses with proof objects.

Does "proof objects" here refer to the term the elaborator send to the kernel?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@pandaman yes. In Lean, those have the type docs#Lean.Expr.

[Kevin Buzzard]

Ruben Van de Velde said:

Only in the sense that it hasn't happened yet, I imagine

Nonono, the JacobiZariski file makes heavy use of constructions like docs#Algebra.Extension which I'm not sure sinple type theory is equipped to deal with, and its extension to schemes will present even more problems. The issues are mathematical not sociological, but this thread is not the place to talk about them.

[Notification Bot]

11 messages were moved here from #general > Lean in the wild by Johan Commelin.

[Johan Commelin]

@Kevin Buzzard You challenged them with schemes, and they did that. I think they've provided ample evidence that complicated objects can be formalized in Isabelle. There certainly isn't any theoretical obstruction.

[Kevin Buzzard]

That is true, I was skeptical about schemes and they showed that this could be done, although they did not use the standard development of rings to do it. Perhaps they can do cotangent complexes somehow.

[suhr]

It's a common theme: mathematicians worry about foundations not being powerful enough, while in practice they are usually way too powerful. One can do a lot in a foundation weaker than ZFC. For example, people do algebraic geometry in Cubical Agda (https://www.youtube.com/watch?v=DJNisW5m1BA), which is as weak as one can get in terms of proof theoretic strength.

[Patrick Massot]

This is not the common theme appearing in this conversation: the common theme is people talking past each other because half of the conversation is about what is doable and half of the conversation is about what is doable in a nice as productive way.

[Kevin Buzzard]

Andrew Yang said:

import Mathlib

open TensorProduct

variable {R R' S : Type*} (R'' : Type*) [CommRing R] [CommRing R'] [CommRing R''] [CommRing S]
    [Algebra R R'] [Algebra R' R''] [Algebra R R''] [IsScalarTower R R' R''] [Algebra R S] (e : R' ⊗[R] S)

#synth IsScalarTower R R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}))

This is the usual problem (which could be fixed):

            [] [0.000072] new goal AddCommMonoid (R' ⊗[R] S ⧸ Ideal.span {e}) ▶
            [] [0.003458] ✅️ apply @ESeminormedAddCommMonoid.toAddCommMonoid to AddCommMonoid (R' ⊗[R] S ⧸ Ideal.span {e}) ▶
            [] [0.174059] ✅️ apply @topologicalRingQuotientTopology to TopologicalSpace (R' ⊗[R] S ⧸ Ideal.span {e}) ▶
            [] [0.000225] ✅️ apply @UpgradedStandardBorel.toTopologicalSpace to TopologicalSpace (R' ⊗[R] S) ▶

etc etc. But it does make the point that sometimes typeclass inference can be slow (because nobody separated the norm and algebra heirarchies yet).

[Kenny Lau]

we should lower the instance priority on ESeminormedAddCommMonoid.toAddCommMonoid definitely

[Kevin Buzzard]

But this is exactly the point Andrew is making -- we can fix things by fiddling around with the numbers but that is hardly a good user experience.

[Matthew Ballard]

Did we stop unbundling?

A lot of this still very much experimental and we are learning the best patterns. Perhaps that sentiment applies to the other languages also.

[Yuyang Zhao]

I think we're waiting for lean4#8279.

[Matthew Ballard]

With P-low I would assume that is dead.

[Bryan Gin-ge Chen]

Based on my reading of the contributing guidelines, I don't think P-low means it's dead; it just means that someone outside the FRO will have to do the work for it (and then we may have to wait a long time for the FRO to get around to reviewing it).

[Christian Merten]

For PRs and RFCs, the priority reflects our commitment to reviewing them and getting them to an acceptable state.

I think this is pretty clear unfortunately.

[Lawrence Wu (llllvvuu)]

Correct me if I’m wrong: it seems that unexpected slowness in Lean is mostly in mathlib and downstream of mathlib, and is often due to searching mathlib’s typeclass hierarchy. So the complaint about Lean itself would mostly be that it is even possible to create a typeclass hierarchy which is slow to search. The most naive “solution” would be to just not have typeclasses.

1. How does this relate to dependent type theory?
2. What is the equivalent of typeclasses that provides the same magic but is impossible to make slow?

[Christian Merten]

It is not about "it is possible to create a hieararchy which is slow to search", but rather about "it is hard to create a hierarchy which is fast to search".

[Lawrence Wu (llllvvuu)]

Is it hard because of dependent types? Why? (unification? locales are better but somehow incompatible?)

[Aaron Liu]

it's because we have all these typeclasses

[Aaron Liu]

it ends up with many many was to derive the same thing so it takes a while to check them all

[Aaron Liu]

For example, to derive Add, you have to check all of these

• docs#ENormedAddCommMonoid
• docs#Ring
• docs#IdemSemiring
• docs#SubtractionMonoid
• docs#SubtractionCommMonoid
• docs#DivisionSemiring
• docs#DivisionRing
• docs#Distrib
• docs#NormedAddCommGroup
• docs#AddMonoid
• docs#ConditionallyCompleteLinearOrderedField

etc.

[Kenny Lau]

would "forward typeclass inference" proposed some time ago help with this problem?

[Lawrence Wu (llllvvuu)]

Right, I guess this thread lost the original context (#general > Lean in the wild @ 💬 ), I'm trying to figure out how Lean/dependent type theory is to blame for this / how Isabelle doesn't end up in this situation.