竞赛/平台指南

数学蒸馏挑战赛：第二阶段 Playground（试验场）使用指南

Mathematics Distillation Challenge: Stage 2 Playground Guide

竞赛/平台指南🎤 SAIR 频道旁白讲解（未署名解说者）⏱ 2:36👁 NA

▶ 在 YouTube 观看

一段约 2 分半的官方教程，演示如何在 SAIR「数学蒸馏挑战赛——等式理论（Equational Theories）」第二阶段的 Playground 中创建、运行和调试求解器（solver），并说明正式比赛的两条赛道与提交规则。

核心要点

Playground 仅用于调试与验证求解器，不计入正式比赛成绩。
使用前须先注册服务器账号；系统每天免费发放额度（credits），于 UTC 午夜重置。
操作流程：进入比赛详情页 → 打开 Playground → 创建/选择 solver → 选模型 → 选问题 → 点击 run 运行。
运行结束后结果面板会显示 judge 裁决、Lean 输出、运行时间和模型调用记录，用于迭代改进。
第二阶段正式比赛设 solo 与 marathon 两条赛道，可任选其一或同时参加。
提交的 Python 求解器文件大小不得超过 500 KB。

分章详解

开场与定位：Playground 是什么

视频开宗明义介绍「数学蒸馏挑战赛——等式理论（Mathematics Distillation Challenge, Equational Theories）」第二阶段的 Playground（试验场）。
明确 Playground 只用于调试（debugging）和验证（validation），不计入官方竞赛分数，目的是降低试错成本。

准备工作：账号与每日免费额度

开始之前必须先注册服务器账号（server account）。
系统每天发放免费额度（free credits），额度在 UTC 午夜（midnight UTC）自动重置，方便用户持续测试。

进入 Playground 并创建求解器（solver）

路径：先进入比赛详情页（competition details page），再选择 playground 打开页面。
在 solver 区域可创建或选择求解器，点击「add new」新建。
可直接在编辑器中写代码，也可上传本地 .python 文件。
求解器本质是用户自己的 Python 解题程序，可包含搜索逻辑（search logic）、决策策略（decision strategies）和提示词（prompts），但最终须给出判定结果。

配置并运行测试

选择本次测试要使用的模型（model）。
从公开题集（public problem set）中选题，或添加自定义问题（custom problem）。
确认 solver、模型、问题三者就绪后，点击 run 启动测试。

查看结果并迭代

测试完成后，结果面板会显示：judge 裁决（verdict）、Lean 输出、运行时间（run time）和模型调用记录（model call records）。
用户可据此反馈定位问题、验证想法，反复重跑测试并对比不同策略的效果。
Playground 的核心价值在于在正式提交前快速发现问题、验证思路、逐步提升求解器的稳定性。

正式比赛规则：赛道与提交限制

正式的第二阶段比赛提供两条赛道：solo（单人）和 marathon（马拉松）。
参赛者可只选一条赛道，也可同时参加两条。
无论选哪条赛道，提交的 Python 求解器都不得超过 500 KB。
视频结尾鼓励用户在 SAIR Playground 中开始试验，为正式提交做准备。

关键引述

“「Playground 只用于调试与验证，不计入你的官方比赛成绩。」（The playground is only for debugging and validation and does not count towards your official competition score.）”— SAIR 解说旁白

“「系统每天发放免费额度，并在 UTC 午夜重置。」（The system provides free credits every day, which reset daily at midnight UTC.）”— SAIR 解说旁白

“「Playground 的核心价值，是帮助你在正式提交前快速发现问题、验证想法，并逐步提升求解器的稳定性。」（The core value of the playground is to help you quickly identify issues, validate ideas, and gradually improve the stability of your solver before making an official submission.）”— SAIR 解说旁白

“「无论选择哪条赛道，你提交的 Python 求解器都不得超过 500 KB。」（Regardless of which track you choose, your submitted Python solver must not exceed 500 kilobytes.）”— SAIR 解说旁白

术语 / 人物

数学蒸馏挑战赛（Mathematics Distillation Challenge） — 由 Damek Davis、Terence Tao 与 SAIR 基金会发起的竞赛，旨在把「等式理论项目」中约 2200 万条通用代数判定结果『蒸馏』成简短、可读的『速查表（cheat sheet）』，以辅助 LLM 判断等式是否成立。

等式理论（Equational Theories） — 源自 Tao 2024 年发起的 Equational Theories Project，借助 Lean 形式化与自动定理证明，系统判定约 2200 万条代数律之间的蕴含关系。

Playground（试验场） — 竞赛平台提供的调试沙盒，可在不影响正式成绩的前提下编写、运行并验证求解器。

Solver（求解器） — 参赛者编写的 Python 解题程序，可包含搜索逻辑、决策策略和提示词，最终输出对问题的判定。

Lean — 一种形式化证明语言/定理证明器；Playground 结果面板会展示 Lean 输出以供核验。

solo / marathon 赛道 — 第二阶段正式比赛的两种参赛模式，可任选其一或同时参加。

背景补充

SAIR（Scientific AI Research，科学与 AI 研究基金会）由 Terence Tao（陶哲轩）等人参与创立，Tao 担任理事会成员。该「数学蒸馏挑战赛——等式理论」是 SAIR 的首个竞赛，由 Damek Davis 与 Terence Tao 共同组织，延续了 Tao 2024 年发起的 Equational Theories Project（用 Lean 形式化判定约 2200 万条通用代数真假命题）。第一阶段已完成并产出多份有效『速查表』，排名靠前的参赛者进入更难的第二阶段——不仅要给出真/假判断，还要生成形式化证明或有效反例。

适合谁看

适合已注册或计划参加 SAIR 数学蒸馏挑战赛第二阶段的参赛者，以及对自动定理证明、Lean 形式化与 AI 辅助数学竞赛平台操作感兴趣的开发者与研究者。