Prepared by: Amey Thakur
Competition: Stage 1 · Stage 2
Welcome to the long-term research repository for the SAIR Mathematics Distillation Challenge. This repository contains all research, analysis, source codes, and submission artifacts for both Stage 1 and Stage 2 of the competition.
The repository is structured to separate the completed Phase 1 work from ongoing Phase 2 research.
Stage 1 focused on human-readable heuristics, prompt engineering, and producing concise cheatsheets.
- prompts/: Canonical prompt templates for Stage 1.
- cheatsheets/: Distilled knowledge artifacts (e.g., magma cheatsheet).
- analysis/: Technical analysis of magma theories and problem subsets.
- scripts/: Python tools for data profiling and analytics.
- sources/: Raw source data and external dependencies (including Lean 4 source repos).
Stage 2 transitions into automated theorem proving, counterexample generation, and Lean 4 verification.
- architecture.md: System architecture for the solver.
- research.md: Research report detailing judge interaction, Lean verification, and budget optimization.
- solvers/: Active production solvers featuring Triage, AST Analysis, and SymPy SAT counterexample generation.