SAIR Mathematics Distillation Challenge Stage 2 将“给答案”升级为必须提交 Lean proof / counterexample certificate

SAIR 于 4 月 23 日开放 Stage 2 预注册，围绕 Equational Theories 构建 certificate-first competition：给定两条 magma equations，solver 不能只输出 true/false，而必须对 true implication 提交 Lean 4 proof，对 false implication 提交有限或无限 magma counterexample certificate，由 deterministic Lean judge 自动裁决。Stage 2 同时提供 Solo 与 Marathon tracks，并公开 judge 与 submission harness。