Mathematics Distillation Challenge – Equational Theories

Terence Tao and Damek Davis have launched the Mathematics Distillation Challenge, hosted by the SAIR Foundation. Building on the Equational Theories Project (ETP) which formally verified over 22 million true-false problems in universal algebra, the challenge asks contestants to create a compact 'cheat sheet' (≤10KB) that helps small, cheap AI models improve their accuracy on these problems beyond the ~50% random-chance baseline. Stage 1 runs until April 20, testing submissions against 1200 problems (1000 easy, 200 hard). Top 1000 submissions advance to Stage 2, which will require generating proofs or counterexamples using more advanced models. The goal is to distill mathematical problem-solving techniques into human-readable, transferable knowledge.