Mathematics Distillation Challenge – Equational Theories

Mathematics Distillation Challenge – Equational Theories(terrytao.wordpress.com)

110 points by picafrost 65 days ago | 5 comments

_ache_ 64 days ago |

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

steppi 64 days ago | |

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.

[1] https://mathoverflow.net/questions/64071/what-does-the-term-...

tux3 64 days ago | |

The goal isn't to improve the AI performance using the cheat sheet, it's to produce a cheat sheet at all that efficiently distills intuition about these 22 million results.

Presumably if it's written in plain text and useful to the AI, there may be some relevant information in there that will be interesting for humans too.

_ache_ 64 days ago | | |

As I say, I understand the goal of having a cheat sheet that can distills a big chunk of math. But that distillation would have been better done by a neural network instead of the creation of a prompt (fine-tuning or pure distillation). But studying that neural network will be harder.

It's explicitly stated that the goal is to improve performance of cheap models but I assume, like you did, that they are hopping that the plain text may be useful to humans too.