Erdős Problem 176 — exact small values of the discrepancy threshold N(k,2) with machine-checkable DRAT certificates

Exact two-sided values of N(k,2) for k = 2..12 (3, 9, 13, 22, 11, 49, 57, 65, 19, 112, 45) — the least N such that every ±1 coloring of {1,…,N} forces a k-term arithmetic progression with |sum| ≥ 2 (Erdős Problem 176, erdosproblems.com/176). For each k ≤ 12 the bundle ships a DIMACS instance and a DRAT UNSAT proof verified by drat-trim (CaDiCaL 1.7.4 + drat-trim v05.22.2023, containerized and pinned), plus an exact-evaluator-checked witness coloring at N−1: the first publicly available machine-checkable proof objects for these values, independently confirming Quantiterate LLC (2026-06-19, Zenodo 10.5281/zenodo.20763838) for odd k and Spencer (1973) for even k. Also included: one-sided lower bounds for k = 13..25 (evaluator-verified witnesses; N(15,2) ≥ 225, N(23,2) ≥ 508, others in the bundle), the exact integer evaluator, and the full audit harness (dual-engine UNSAT re-runs + solver-free brute force for k ≤ 6). Verification: one-command replay, exit 0, OVERALL PASS. Developed with AI assistance under a machine-verification gate; see README for the production chain and honest labels.