High-Throughput Lean 4 Autoformalization Model for Local Inference

There's not yet a Lean Mathlib signals library?

Is that a good use case for autoformalization?