Lots of people are talking about that, and have been for a while. Autoformalisation is clearly going to be a big deal, so mathematicians have been discussing it seriously, and using it where resources allow. A fine-tuned distilled model that could do it on high-end consumer hardware could really help.

Edit: There's also quite a bit of learning needed to use the tools, and to understand enough to confirm that the theorem being verified is what you think. And of course a lot of maths can't yet be expressed in Lean as the foundations haven't been built up enough.

▲

cyanydeez 4 hours ago | parent | next [-]

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

	▲	mkl 3 hours ago \| parent [-]
		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.

▲

mr-pink 4 hours ago | parent | prev | next [-]

you dont have to take headlines literally.

	▲	bloppe 4 hours ago \| parent [-]
		Most people do, so the literal interpretation matters a lot

▲

aaron695 3 hours ago | parent | prev [-]

[dead]