Cycles through three proof strategies and shows how each transforms the original goal into a different logical task: (1) Direct proof builds a chain of implications from premises to the goal, (2) Contradiction assumes the negated goal and animates the derivation of an explicit contradiction (⟂) to conclude the original goal, and (3) Induction breaks a universal claim (∀n) into a base case and an inductive step (n→n+1), then highlights the resulting universal conclusion.
Uses a 4px snap-to-grid helper for a blocky aesthetic, time-based cycling (4.2s) across the three modes, and easing-driven progress bars. Draws only with Canvas 2D primitives (rects, strokes, monospace text) in a green-on-black palette; includes pulsing highlights and moving tokens to emphasize the active logical transformation.