Formal proof triumphs. Read the full story