Damek Davis and I have launched a "distillation challenge", to see how well the 22 million implications in universal algebra generated by the Equational Theories Project can be condensed down to a single "cheat sheet" prompt that a low-powered LLM can use to answer these questions as accurately as possible. The challenge is hosted by the SAIR foundation at https://competition.sair.foundation/competitions/mathematics-distillation-challenge-equational-theories-stage1/overview and some further discussion is at https://terrytao.wordpress.com/2026/03/13/mathematics-distillation-challenge-equational-theories/
