The existence of an undiscovered soundness bug doesn't make everything proven in Lean illicit. The proof would have to exploit the bug. People build houses on sound foundations even though the tectonic situation under them might not be sound.
> Because of these properties, the final backstop has to be humans...
The post has clearly stated that the work on Lean's underlying metatheory is not done, and requires more work. It's not inconceivable that computer formal verification could reach the trustworthiness of math itself.
> Because of these properties, the final backstop has to be humans...
The post has clearly stated that the work on Lean's underlying metatheory is not done, and requires more work. It's not inconceivable that computer formal verification could reach the trustworthiness of math itself.