Modified benchmark, tested using hyperfine:

Benchmark 1: .lake/build/bin/benchmark
  Time (mean ± σ):     699.9 ms ±   9.7 ms    [User: 684.2 ms, System: 12.5 ms]
  Range (min … max):   687.7 ms … 721.5 ms    10 runs
 
Benchmark 2: ./a.out
  Time (mean ± σ):     561.1 ms ±   6.5 ms    [User: 531.4 ms, System: 26.5 ms]
  Range (min … max):   555.2 ms … 574.9 ms    10 runs
 
Summary
  ./a.out ran
    1.25 ± 0.02 times faster than .lake/build/bin/benchmark

Original repo at https://github.com/lacker/lean4perf

lean4perf

Some performance testing of Lean 4. I only tested on Linux. The benchmark just inserts a lot of string -> number pairs into a hash map.

To run the Lean 4 benchmark:

# Install Lean 4
elan install leanprover/lean4:4.0.0-m1

# Run the benchmark
time lean --run benchmark.lean

47 seconds on my machine.

To run the equivalent C++ benchmark:

# Compile. I assume you already have gcc installed
g++ -O3 benchmark.cpp

# Run the benchmark
time ./a.out

7 seconds on my machine.