Already saw it on Mastodon yesterday. A better presentation is in the other link. (<a href="https://competition.sair.foundation/competitions/mathematics-distillation-challenge-equational-theories-stage1/overview" rel="nofollow">https://competition.sair.foundation/competitions/mathematics...</a>)<p>I understand the idea of a distillation challenge but it really feels like the poor man's solution to a problem that could be better solved by training a LLM and analysing the layers.
In the end, as I value a condensed "cheat sheet", if the goal is to improve open-source model. A better approach seems to recreate the AlphaProof system, longer to do, but more efficient. The path taken by mathematicians now is agentic system with general LLM.<p>- Masto: <a href="https://mathstodon.xyz/@tao/116225525978210807" rel="nofollow">https://mathstodon.xyz/@tao/116225525978210807</a><p>- AlphaProof: <a href="https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/" rel="nofollow">https://deepmind.google/blog/ai-solves-imo-problems-at-silve...</a><p>- AlphaProof description: <a href="https://www.nature.com/articles/s41586-025-09833-y" rel="nofollow">https://www.nature.com/articles/s41586-025-09833-y</a>
It seems like the lift in the open-source models is being used as a proxy metric, and the core goal is a human understandable yoga [1] for approaching these kinds of equational proofs in universal algebra.<p>[1] <a href="https://mathoverflow.net/questions/64071/what-does-the-term-yoga-mean-in-mathematics" rel="nofollow">https://mathoverflow.net/questions/64071/what-does-the-term-...</a>
[dead]