[Paracompact]

I haven't looked into the code, but Lean being so slow may be misleading depending on how you benchmarked it. IMO the fairest test is how "Lean code" (or Rocq code, etc.) is actually run, which is as native C code following extraction.

Given the sane C defaults that are applied by code extraction techniques, the delta really shouldn't be so great. But it's a common pitfall to torture one's own verified code in order to get it proven, and I'm also not sure how good of support there is for parallelism.