11 ms·
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
by mkl 6d ago
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.
- mr-pink 6d agoyou dont have to take headlines literally.
- bloppe 6d agoMost people do, so the literal interpretation matters a lot
- cyanydeez 6d agoQwen3.8-Flash-Next loads in 60gb on quant4. Thats pretty close to consumer hardware.
- mkl 6d agoIs 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 6d agoso far unsloth only has https://unsloth.ai/docs/models/qwen3.8/train 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.
- aaron695 6d ago[dead]