3 ms·High-Throughput Lean 4 Autoformalization Model for Local Inference4 points by matteohorvath 1mo agowesturner 1mo agoThere's not yet a Lean Mathlib signals library? Is that a good use case for autoformalization?