Every known way to get a proof of False accepted in Lean 4 and Rocq/Coq, organised by what the route costs: paradoxes of type theory, sanctioned escape hatches, kernel defects, and audits that found nothing.