Mathematics Distillation Challenge – Equational Theories

2 days ago

Mathematical research traditionally involves small groups of professional mathematicians working on deep problems.
A complementary approach involves collaborating with a broad community on mathematically interesting problems using modern technologies like AI.
Examples of such collaborations include Polymath projects, collaborative formalization projects, and the Equational Theories Project (ETP).
The ETP used Lean formalization and automated theorem provers to solve over 22 million true-false problems in universal algebra.
A new project aims to distill the ETP's results into a concise, human-readable 'cheat sheet'.
The project includes a competitive challenge to design a cheat sheet (≤10KB) that improves the performance of cheap AI models on true-false problems.
Stage 1 of the challenge involves testing cheat sheets on a public set of 1200 problems (1000 easy, 200 hard).
Top 1000 submissions will advance to Stage 2, which involves more advanced models and providing proofs or counterexamples.
The competition is coordinated on a Zulip channel, with submissions due by April 20.
Future challenges may focus on other mathematical problem classes and cooperative approaches.

Hasty Briefsbeta