- 132comments
- 7comments
- 79comments
- 24comments
- 106comments
- 212comments
- 114comments
- 41comments
- 181comments
- 558comments
- 6comments
- 76comments
- 4comments
- 23comments
- 68comments
- 3comments
- —discuss
- 9comments
- 176comments
- 3comments
- 13comments
- 158comments
- 77comments
- 118comments
- 1comments
- 49comments
- 80comments
- 1comments
- 197comments
- 62comments
Seems like this would have strong implications for distillation and/or smaller types of transformers!
How? I don't see it. (I'm familiar with the ML side, not the combinatorics side.)
Actual meat: https://arxiv.org/abs/2510.20765
I am not a mathematician but are most papers now accompanied by a lean proof?
Is there a central repository of lean proofs shared by mathematicians like an npm repository of JavaScript packages?
Does it all depend on a stupid is-odd package in the end?
It's new but there is actually a registry now: https://palomar-registry.org/
LLMs have gotten good at creating Lean proofs so the are much more common but not universal. And they depend on https://github.com/leanprover-community/mathlib4