On: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

[cyanydeez]

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

[mkl → cyanydeez]

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.

[cyanydeez → mkl]

so far unsloth only has https://unsloth.ai/docs/models/qwen3.8/train which is the 27B model. It also getting pretty close to what you'd need.

I wouldn't be surprised if someone is trying it.