Qwen3.8-Flash-Next loads in 60gb on quant4. Thats pretty close to consumer hardware.

Is it any good at autoformalisation? I think it's likely to take focused fine-tuning to get something small enough that is still good at that.