Already saw it on Mastodon yesterday. A better presentation is in the other link. (https://competition.sair.foundation/competitions/mathematics...)

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.

- Masto: https://mathstodon.xyz/@tao/116225525978210807

- AlphaProof: https://deepmind.google/blog/ai-solves-imo-problems-at-silve...

- AlphaProof description: https://www.nature.com/articles/s41586-025-09833-y