I think this must be wrong. If the kernel is free of bugs then it's not going to...

		alimw 6 days ago \| parent \| context \| favorite \| on: Lean proved this program correct; then I found a b... I think this must be wrong. If the kernel is free of bugs then it's not going to pass a proof of false no matter what the Lean compiler gets up to.

		help