Comment by anonymous_user9

Yes, for all we know they're exploiting a bug in Lean.