Registry · Theorem
III.T65
tau-effective
formalized
III.T65 — ABC at Primorial Levels
ABC at primorial levels: for each stage k, all coprime pairs (a,b) with a,b < min(M_k, 20) satisfy c < rad(abc)². Finite verification of ABC for small values. Verified at depth 3.