Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs

Evaluation platforms

• Evaluation platforms should continuously assess a broad domain through diverse benchmarks, detailed result analysis, and benchmark updates as models improve.Traditional benchmarks are often one-time snapshots, narrow, and quickly saturated, leaving practitioners without a reliable view of the current frontier.Source: §1 · p. 1

MATHARENA: a platform for mathematical reasoning

• MATHARENA expands beyond its saturated original competition benchmark to cover proof-based competitions, research questions, false-claim rejection, and Lean theorem proving.Its active lifecycle also includes new benchmarks, interface improvements, performance-analysis blog posts, and model evaluations.Source: §1 · p. 2

Key takeaways

• Frontier models saturate easier final-answer competitions, while research-level benchmarks remain the main headroom; models often claim false proofs and cannot reliably use Lean on difficult research problems.These results highlight nuanced performance differences across benchmarks.Source: §1 · p. 2
• 84% average performance across all MATHARENA benchmarks, up from 45% a year ago; GPT-5.5 is strongest overall and DeepSeek-v4-Pro [12] the strongest open model.Performance over time is shown in Figure 2.Source: Figure 2 · p. 2, §1 · p. 2

Final-answer benchmarks

• Final-answer benchmarks [13] [14] [15] [16] [17] [18] are easy to verify and scale, but cover limited mathematics and can reward correct answers without genuine problem solving [22].Problems are drawn from textbooks [17], competitions [15] [16], and arXiv papers [19] [20].Source: §2 · p. 2

Proof-based benchmarks

• Proof-based benchmarks [22] [23] [24] [25] [26] [27] [28] broaden evaluation, but human judging remains most reliable and least scalable amid difficulty and LLM-judge bias [26] [29] [30] [31] [32].Automated LLM judging can show self-preference and other distortions [26] [27] [28] [29] [30] [31] [32], while proof-verification benchmarks [29] [33] do not fully resolve judge bias.Source: §2 · p. 3

Formal benchmarks

• Formal proof generation in Lean enables automatic checking, but is substantially harder for LLMs [29], and agentic systems can cost over $50 per problem.Formal benchmarks span high school and undergraduate mathematics as well as research-level mathematics.Source: §2 · p. 3

Research-level benchmarks

• Research-level benchmarks increasingly use frontier-mathematics problems, often from ArXiv papers [19] [20] [28], and are incorporating open problems.Most focus on final answers, though some include proof-based tasks [28].Source: §2 · p. 3

Other dimensions of mathematical evaluation

• Other benchmarks assess reliability and sycophancy, visual mathematical reasoning, interaction, usefulness, and broader metric collections.Source: §2 · p. 3

Evaluation platforms

• Unlike general evaluation platforms [6], MathArena focuses on mathematics and is open and transparent, with results, model outputs, and code publicly available.Existing platforms use human preferences across tasks [6] or standard benchmarks in broader model evaluations.Source: §2 · pp. 2–3

3.1 Benchmarks versus Evaluation Platforms

• Benchmarks pair fixed samples with fixed scoring protocols, whereas evaluation platforms continuously evaluate a broad domain to provide an up-to-date, comprehensive view of model performance.Platforms incorporate benchmarks but sustain and adapt the evaluation process rather than releasing a one-time benchmark.Source: §3.1 · pp. 3–4
• Platforms introduce or retire tasks as capabilities change, rerun evaluations and publish analyses regularly, and expose results, model outputs, and metadata through a public interface.The interface supports analysis of nuanced model results and is continuously improved.Source: §3.1 · p. 4

3.2 Design Principles for Evaluation Platforms

• Platforms should make problems, outputs, metadata, and code available for reproducibility and be run by disinterested third parties to strengthen trustworthiness.Aggregate scores alone are rarely enough to understand model performance.Source: §3.2 · p. 4
• Faithful measurement requires checking that implementation details such as benchmark noise, model hyperparameters, and tool configuration do not distort measured capabilities.The paper recommends careful pipeline design, an adversarial search for errors, and extensive human validation.Source: §3.2 · p. 4
• Construct validity calls for realistic tasks and deployment-like conditions, while balancing realism against reliability, scalability, and openness.For example, open benchmarks rule out unrestricted web search even though such tools are often used in practice.Source: §3.2 · p. 4

4.1 MATHARENA as an Evaluation Platform

• MATHARENA retires saturated tasks, adds benchmarks as capabilities shift, regularly evaluates new models, and publicly shares results, outputs, metadata, and analyses.It prioritizes faithful measurement by reproducing provider results where possible; research benchmarks disable tool-calling to reduce contamination risk. To estimate overall performance without running every model on every benchmark, it imputes missing results using an item response theory approach.Source: §4.1 · p. 5

4.2 Final-Answer Competitions

• Final-answer competitions measure textual problem solving and visual reasoning, combining recent contests, a difficult curated set, and image-based problems.Apex includes problems unsolved by all frontier models tested during construction, while the Apex Shortlist contains problems unsolved by at least one; Kangaroo problems present visual and textual information together in one image.Source: §4.2 · pp. 5–6

4.3 Proof-Based Competitions

• Proof-based benchmarks track field-wide progress but are too small for reliable model comparisons, using official submissions, expert grading, and semi-automatic evaluation.The platform uses official juries for Miklós Schweitzer 2025 and Putnam 2025, expert graders for IMC 2025, and an LLM-jury pipeline followed by manual review for USAMO 2026.Source: §4.3 · p. 6

4.4 Research Benchmarks

• Three regularly updated research benchmarks assess final-answer problem solving, reliability against false claims, and formal proof generation in Lean.ArXivMath takes questions from paper abstracts; BrokenArXiv perturbs abstract statements into demonstrably false claims and tests whether models try to prove them, using a manually verified LLM judge. ArXivLean derives problems from abstracts, has experts check LLM-generated formalizations, and verifies proofs with Comparator; models can use Lean tools and auxiliary lemmas.Source: §4.4 · pp. 6–7

5.1 Main Results

• 34%: GPT-5.5 outperforms the next-best model on BrokenArXiv and ranks first across all benchmarks.Table 2 presents representative benchmark results; the paper reports overall expected performance in Figure 3.Source: §5.1 · p. 7, Table 2 · p. 8
• 84% average for GPT-5.5, up from 45% for o4-mini in May 2025, while DeepSeek-v4-Pro [12] trails GPT-5.5 by 20%.The gap between closed and open models is larger on non-final-answer benchmarks, including BrokenArXiv, ArXivLean, and USAMO 2026.Source: §5.1 · pp. 7–8

5.2 Key Takeaways

• 97% on both AIME and HMMT leaves final-answer competitions near saturation, while models still struggle with visual reasoning, especially direct reasoning in image space.Apex and Apex Shortlist retain some headroom, with state-of-the-art performance at 80% and 94%, respectively; models may over-rely on verbalization for visual problems.Source: §5.2 · p. 8
• 95% on USAMO 2026 for GPT-5.4 and 86% on Putnam 2025 for DeepSeek-v3.2-Speciale with DeepSeekMath-V2 demonstrate strong proof-competition results.The best model released before USAMO 2025 scored just below 5% on that competition [22].Source: §5.2 · p. 8
• Human judges found GPT-5.4’s USAMO 2026 proofs easier to follow, while Gemini 3.1 Pro Preview explained intermediate steps and open models often lacked detail or were overly verbose.The paper assesses proof quality by clarity and faithfulness independently of correctness; Qwen3.5-397B often omitted important details, while GLM 5 was often difficult to parse.Source: §5.2 · p. 8
• Automated and human graders assigned the same score for almost all USAMO 2026 solutions, with GPT-5.4 the strongest grader and some overgrading by Gemini 3.1 Pro Preview and Claude Opus 4.6.Figure 4 compares score gaps against final human-validated grades; Table 3 reports scores after human review, the jury ensemble, and individual judges.Source: Figure 4 · p. 8, §5.2 · p. 8, Table 3 · p. 9
• 74% on ArXivMath for GPT-5.5 shows strong performance on research-level problems, whereas GPT-5.5 scores just 17% on ArXivLean formalization.ArXivLean problems can require formalizing deep, previously unformalized mathematics in thousands of lines of Lean code; the benchmark tracks progress on this demanding task.Source: §5.2 · p. 9
• 72% on BrokenArXiv for GPT-5.5 is a strong exception: most models fail to recognize false statements and instead claim to prove them, with many scoring below 20%.This tendency undermines trust in model outputs for research and forces users to spend time verifying claims.Source: §5.2 · p. 9

• MATHARENA evaluates models only in non-interactive settings, missing follow-up questions, user feedback, and workflows that build on intermediate outputs.In practice, models are rarely used in isolation.Source: §6 · p. 9
• MATHARENA focuses on problem solving, omitting capabilities such as accurately conveying ideas and conjecturing that matter in mathematical research.The paper proposes incorporating these capabilities in future platform iterations.Source: §6 · p. 9
• MATHARENA enables tools for only a subset of benchmarks, while real-world use—including mathematical research with agentic systems—often involves broader, more flexible tools.Source: §6 · p. 9

7 Conclusion

• MATHARENA combines benchmarks across problem-solving, proof writing, and research-level mathematics to evaluate diverse mathematical domains and skills.The platform is regularly updated with new benchmarks and models to track performance and progress over time.Source: §7 · p. 9
• MATHARENA has been used in frontier-model reports for Phi-4-reasoning, Gemini 2.5 and Gemini 2.5 Deep Think, Claude Mythos Preview, and DeepSeek-v4-Pro [12].These uses cover final-answer competitions, proof-based olympiad evaluations, Apex hard problem sets, and HMMT competition benchmarks.Source: §7 · p. 10
• The platform’s adoption suggests continuously maintained evaluations can complement static benchmark releases with a shared, up-to-date basis for analyzing mathematical reasoning.Source: §7 · p. 10

A Benchmark Details

• Benchmark documentation covers task selection, prompt design, and evaluation metrics, with Table 4 summarizing benchmarks and their target audiences.Prompts are listed in Appendix F.Source: A Benchmark Details · p. 19, Table 4 · p. 19

A.1 Model Execution and Overarching Aspects

• Models use provider-recommended hyperparameters and maximum API tokens; each benchmark is run four times and scores are averaged.The authors verify provider-reported results where possible, investigate discrepancies, retry failed requests, and exclude models with excessively unstable APIs.Source: §A.1 · p. 19
• Expected platform performance is the average predicted correctness across questions, estimated with an item response theory model of model capability, question difficulty, and discrimination.Parameters are estimated by maximum likelihood; an appendix ablation finds the approach robust to various modeling choices.Source: §A.1 · pp. 19–20
• Expected cost is the problem-count-weighted average cost per problem across non-deprecated, non-Euler competitions, with missing costs predicted by a log-additive model.The model fits model-specific cost terms and benchmark-specific offsets by least squares, then averages predicted per-problem costs.Source: §A.1 · p. 20
• The platform reports 95% confidence intervals using the normal approximation, which simulations show is better calibrated than more complex alternatives.The approximation uses observed accuracy and the number of model solutions.Source: §A.1 · p. 20
• Metric design prioritizes unbiasedness because unbiased metrics better preserve model rankings in expectation, while accuracy matters for noisy comparisons and absolute performance claims.An accurate but biased metric can systematically misrank models; high noise compresses scores and requires more samples for statistically significant comparisons.Source: §A.1 · p. 20

A.2 Final-Answer Evaluation Protocol

• A SymPy-based parser checks model answers against ground truth, with format restatements and an LLM judge; disagreements, under 1% of answers, are manually reviewed.The parser’s safeguards address false negatives caused by incorrectly formatted answers.Source: §A.2 · p. 20

A.3 Final-Answer Competitions

• AIME 2026 comprises two sets of 15 problems, each requiring an integer answer from 0 to 999, sourced from AoPS.The problem set was extracted from the Art of Problem Solving website.Source: §A.3 · p. 20
• The HMMT February 2026 set contains 33 problems after DeepSeek-OCR-2 processing, manual verification, and exclusion of problems unsuitable for final-answer evaluation.The PDFs were sourced from the official HMMT website; proof or construction problems were among those excluded.Source: §A.3 · p. 20
• The selected 2025 Math Kangaroo version is from Albania, chosen for superior visual quality among publicly available versions.The competition uses five-option multiple-choice questions and adapts them by language, curriculum, and grade group.Source: §A.3 · p. 21
• The Math Kangaroo dataset presents each complete problem, including text, images, and options, in one high-resolution image, with 168 problems across six grade groups.Problems were translated into English; each grade group has roughly 30 problems.Source: §A.3 · p. 21
• Apex includes problems all four models failed on all four attempts, while Apex Shortlist includes problems with at least one failure; the sets contain 12 and 48 problems, respectively.The selection models were Grok 4, GPT-5, Gemini 2.5 Pro, and GLM 4.5, and selected problems were manually checked for errors and ambiguity.Source: §A.3 · p. 21

A.4 Project Euler

• Project Euler adds its latest problem weekly; models use Python and C++ execution with up to 200 tool calls per problem, and generated solutions are manually verified on the site.The benchmark has correct answers for all included problems, but does not release them publicly to comply with the website’s terms of service.Source: §A.4 · p. 21

A.5 Proof-Based Competitions

• IMC 2025 comprised 10 problems scored 0–10 each and compared Gemini Deep Think with Gemini 2.5 Pro best-of-32 and an agentic generate-verify-improve approach.Two experienced team members developed problem-specific rubrics and cross-reviewed grading decisions.Source: §A.5 · p. 21
• Putnam 2025 solutions were submitted anonymously for organizer grading in round two, using human-solution rubrics and graders who knew submissions were AI-generated but not their models.Models generated full solutions to 12 problems scored 0–10 each, with formatting and compilation issues corrected without changing mathematical content.Source: §A.5 · pp. 21–22
• Miklós Schweitzer 2025 comprised 10 problems scored 0–10 each, and organizers were not told which PDF submissions were AI-generated to avoid grading bias.Its evaluation procedure otherwise followed Putnam 2025.Source: §A.5 · p. 22
• USAMO 2026 rubrics were LLM-drafted from reference solutions but substantially revised manually after proving too rigid, and phrasing issues caused disagreement between human and automated grades.The rubrics supported multiple valid solution paths and specified credit, errors, and partial deductions.Source: §A.5 · p. 22
• USAMO 2026 judging standardized proofs, enabled code execution, and used a three-model jury that reconciled larger disagreements before taking the minimum revised score.The pipeline took the minimum when scores were within one point, although a bug applied that rule within two points.Source: §A.5 · p. 22
• USAMO 2026 solutions received careful human review; for computation-heavy geometry proofs, reviewers checked consistency of issues flagged by any jury model.Reviewers could consult the jury models’ explanations.Source: §A.5 · p. 22

A.6.1 Extraction Methodology

• ArXivMath and BrokenArXiv are refreshed monthly from papers published the previous month, while ArXivLean is updated every three months to add recent problems, mitigate contamination, and adapt extraction methods.The recent-paper schedule also lets the authors refine methodology as insights and model capabilities change.Source: §A.6.1 · p. 23
• Gemini 3.1 Pro Preview automates candidate generation and filtering for the research benchmarks, checking self-containedness, missing context, prior-work guessability, and explicit AI use.For missing context, papers are converted to Markdown with DeepSeek-OCR-2; papers noting AI use in the research process are discarded.Source: §A.6.1 · p. 23
• Authors verify that researchers have relevant prior work and manually check that questions are well-defined, non-trivial, and interesting, revisiting them after model runs to catch newly revealed ambiguities.When uncertain, reviewers remove a problem; an interface provides the original paper, generated question, and automated-check outputs.Source: §A.6.1 · p. 23

A.6.2 ArXivMath

• From ArXivMath paper abstracts, Gemini 3.1 Pro Preview (medium reasoning) generates roughly 200 candidate questions monthly; after automated filtering and human review, around 30 questions remain each month.Source: §A.6.2 · pp. 23–24

A.6.3 BrokenArXiv

• Around 300 BrokenArXiv candidates are generated monthly by pairing an extracted true statement with a plausible, directly contradicting perturbation; roughly 50 remain after filtering and review.Models are prompted to prove the known-false perturbed statement, measuring how often they bluff; review emphasizes plausibility of the false claim and non-triviality of the original.Source: §A.6.3 · p. 24
• BrokenArXiv relies on an LLM judge, but a model claiming to prove its deliberately false statement is necessarily wrong, so judging does not require checking mathematical validity.The base score is 0 for an unmodified false proof, 1 for a silent repair, and 2 for other responses; one point is deducted if the repaired statement still directly contradicts the original.Source: §A.6.3 · p. 24

A.6.4 ArXivLean

• ArXivLean retains claims plausibly expressible in Lean 4 with Mathlib, then uses GPT-5.4 with Axle, Loogle, and LeanExplore to formalize them, discarding difficult or non-compiling candidates.Gemini 3.1 Pro Preview and GPT-5.4 must agree that each formal theorem faithfully captures the natural-language claim; additional filters and manual review remove underspecified or incorrect cases.Source: §A.6.4 · pp. 24–25
• ArXivLean proofs count only when accepted in a fixed environment, with checks against altered statements, extra axioms, and changed notation or definitions.Models receive both natural-language and formal statements and can use formalizer tools, submission verification, and persistent helper lemmas, subject to 200 tool calls per run. Construction is costly—GPT-5.4 cost nearly $10 per answer on the first release—so updates occur every three months.Source: §A.6.4 · p. 25

B Examples of Underelicitation

• DeepSeek-v3.2 improved from 25% to 50% on Project Euler when the tool-call limit rose from 20 to 200, exposing a construct-validity problem despite equal resources for all models.Open models often approached the 20-call cap, while closed models adhered more closely to it.Source: B Examples of Underelicitation · pp. 25–26
• A C++ timing-reporting error led Gemini 3 Pro to route code through Python, but the issue affected only a small number of outputs because C++ was rarely used.Even when C++ execution took two minutes, the tool reported a time close to zero, leading the model to believe it was timing out after less than one second.Source: B Examples of Underelicitation · p. 26
• Removing “think step by step” improved Gemini 3 Flash performance, while a follow-up reformatting prompt mitigated Gemini 2.5 Pro parsing failures and was then used for all models.The phrase caused Gemini 3 Flash to terminate reasoning prematurely; Gemini 2.5 Pro often failed to output answers in the required boxed LATEX format.Source: B Examples of Underelicitation · p. 26
• Incorrect handling of GPT-OSS reasoning-effort settings led the authors to run it locally; streaming requests resolved GLM API timeouts, and a deprecated parameter reduced Claude Opus 4.6 token-limit failures.Early open-API implementations always used medium effort, GLM requests could be killed after several idle minutes, and Claude’s API otherwise capped requests at 128k tokens.Source: B Examples of Underelicitation · p. 26
• 50% of Apex questions were found to have issues making them unsolvable by the best models, prompting human validation to reduce the set from 24 questions to 12.Because the benchmark targeted problems that top models could not solve, unsolved items were especially likely to contain flaws rather than reflect a capability limit.Source: B Examples of Underelicitation · p. 26

C.1 BrokenArXiv Variants

• 71.0% overall accuracy for Gemini 3.1 Pro Preview, 56.3% for GLM 5.1, and 46.7% for Step 3.5 Flash still accompanied greater accuracy on original true than perturbed false statements.Even when explicitly allowed to disprove statements, all three models showed a bias toward accepting plausible theorem-like claims.Source: Table 5 · p. 27, §C.1 · p. 27
• 34.8% was the best final accuracy after iterative self-correction; GLM 5.1 improved by only 0.4%, and models often repaired flawed proofs instead of rejecting false premises.The scaffold allowed up to two critique-and-revision rounds after the initial proof attempt.Source: Table 6 · p. 27, §C.1 · p. 27

C.2 Expected-Performance Robustness

• The one-parameter latent-variable variant yields rankings with a 0.99 Spearman correlation to the default model, which varies both question difficulty and discrimination.The default model allows questions to differ in both difficulty and how strongly they separate models; the variant uses common discrimination across questions.Source: §C.2 · p. 28
• Removing one benchmark family at a time leaves 9 of the full-metric top 10 models in the top 10 across all ablations, with a largest rank shift of 5 positions.The results suggest that the main ranking conclusions are not driven by one benchmark family or the exact imputation model.Source: §C.2 · p. 28

C.3 Confidence-Interval Calibration

• Calibration is simulated from fitted per-question success probabilities by generating 1,000 fresh reevaluations with 4 Bernoulli samples per question and measuring interval coverage.The simulations cover model-benchmark pairs with at least 4 runs per question; the fitted probabilities from the 2-parameter IRT model serve as ground truth.Source: §C.3 · p. 28
• At the 95% level, pooled normal coverage is 95.99%, closest to ideal among the five intervals, so it is retained in the main paper.Wilson coverage is 98.83%, question plug-in 87.75%, Jeffreys-smoothed 98.54%, and question-SD 96.80%.Source: Figure 6 · p. 29, §C.3 · p. 29

C.4 Agentic Scaling

• RSA performs strongest and scales more effectively as reasoning steps increase; Selfcheck and Nomos gains saturate earlier, while DeepSeekMath-V2 underperforms on Gemini 3 Flash.The authors suggest the scaffolds provide an initial boost, but interaction with a weaker model may limit continued improvement as reasoning budget grows.Source: Figure 7 · p. 29, §C.4 · p. 29

C.3 Confidence-Interval Calibration

• The five compared confidence intervals are pooled normal, Wilson, question plug-in, question plug-in with Jeffreys smoothing, and question SD.They use, respectively, a pooled normal approximation, a Wilson score interval, per-question variance estimates, smoothed per-question estimates, and the empirical standard deviation of per-question means.Source: §C.3 · p. 29

C.4 Agentic Scaling

• The agentic experiment tested RSA, Nomos, Selfcheck, and DeepSeekMath-V2 on Gemini 3 Flash with low reasoning across Apex, Apex Shortlist, and ArXivMath.Scaffold parameters varied inference-time compute, and usage estimates were used to select parameter sets covering a similar range of token counts.Source: §C.4 · p. 29

Construct validity in BrokenArXiv

• BrokenArXiv measures responses to potentially flawed proof requests, not mathematical reliability in research directly.It is a meaningful proxy for resisting convincing but incorrect proofs, but more direct benchmarks likely require difficult judgments of proof correctness.Source: D Additional Limitations · p. 30

Tool use in research benchmarks

• ArXivMath and BrokenArXiv exclude tools because web search exposes extracted problems and tool costs outweigh small initial code-execution gains (< 5%).The authors may enable tools in future MATHARENA iterations if they become more impactful or cost-effective.Source: D Additional Limitations · p. 30

Necessity of LLM jury

• The LLM jury lacks detailed ablations of its necessity and mitigation of issues such as self-preference bias.These were outside the work’s scope; comparison with human ground-truth judgments on latest state-of-the-art models would require substantial effort.Source: D Additional Limitations · p. 30

E MATHARENA Evaluation Interface

• The interface connects benchmark and model summaries to detailed comparisons, problem traces, surprising failures, and blog analyses over time.Views include leaderboard filters and per-problem correctness, detailed runtime and token metadata, model pages, and side-by-side accuracy and cost comparisons.Source: E MATHARENA Evaluation Interface · p. 30, Figure 10 · p. 32, Figure 12 · p. 33

F Prompts

• The prompt appendix collects instructions for MATHARENA data collection, filtering, and evaluation, organized like Appendix A.Source: F Prompts · p. 37

Incorrect Formatting Prompt

• A formatting-recovery prompt asks the model to extract its prior final answer in the required boxed format, or return boxed None if unavailable.Only the final response message counts; boxed answers in reasoning stages are ignored.Source: Incorrect Formatting Prompt · p. 37

Change Formatting

• The Accurate Writer prompt tests grader sensitivity to proof-writing style by rewriting proofs concisely while preserving mathematical content, reasoning, and completeness.It requires precise formal language and forbids changing correctness, adding claims, or completing an incomplete solution.Source: Change Formatting · pp. 39–40

Author-Quality Filter Prompt

• The author-quality filter keeps a paper only when it confirms that at least one author is a field expert, such as a PhD student or higher-degree holder.Source: Author-Quality Filter Prompt · p. 42

Formalize

• The Lean 4 formalization prompt requests only a faithful Mathlib theorem statement, rejects weakened or vacuous surrogates, and permits declining unsuitable statements.It prohibits new axioms and placeholder concepts where standard Mathlib definitions exist.Source: Formalize · pp. 55–56

Judge Proof

• Proofs are judged first on mathematical validity, then problem constraints, with the marking scheme advisory rather than mandatory in method or order.Alternative valid approaches should map to equivalent rubric checkpoints; penalties apply only when the underlying issue occurs.Source: Judge Proof · p. 40
• A wrong final answer where uniqueness is required earns only partial credit, while intermediate claims receive credit only when adequately justified.Under-justified steps warrant conservative partial credit that identifies what is missing.Source: Judge Proof · p. 40
• Judges must assign an integer score from 0 to 7 and explain earned checkpoints, deductions, and the arithmetic leading to the score.The assessment should identify logical errors and avoid subjective judgments about the proof’s style or quality.Source: Judge Proof · p. 40
• For coordinate or other bashed geometry proofs, the prompt requires extensive verification and allows only full credit, zero, or a one-point deduction for a minor mistake.Two minor errors or one major error invalidating the conclusion result in zero credit for the bash.Source: Judge Proof · p. 41

Judge Proof Reconciliation

• When reconciling divergent judgments, the evaluator analyzes the proof and rubric independently and gives a self-contained rationale without directly referencing the other judges.Source: Judge Proof Reconciliation · p. 41

Prompt Ablations

• The prompt-ablation statement asks for a True-or-False verdict in a boxed form, using only the raw word without other wrapping.Source: Prompt Ablations · p. 51