32 points | by ibobev 3 hours ago ago
5 comments
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/
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/
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.)