Benchmarking

Stream: general

[Miguel Raz Guzmán Macedo]

Also, are there any benchmarks of performance vs Coq?

[Mario Carneiro]

It sounds pretty difficult to make any fair comparison

[Mario Carneiro]

there would be a thousand confounding factors in any test

[Mario Carneiro]

In my experience I don't think there is an order of magnitude difference in either direction, but I don't think I could get more specific than that

[Floris van Doorn]

From my subjective experience, executing a single tactic in Lean is a lot faster than in Coq (I wouldn't be surprised if it was an order of magnitude faster). However, the Coq editor modes (I used CoqIDE, but I believe ProofGeneral works the same) ensure that when you are working on proofs, you rarely rerun your tactics, by storing the state in the middle of your tactic proof. On the other hand in Lean, if you change anything in a proof, it will re-elaborate the whole proof, which negates this speed gain.