Lean proved this program correct; then I found a bug