plesiv

It could have military applications; it's hard to imagine any civilian applications.

Beautiful writing style. So light, still eloquent.

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.

Your probability distribution should be flatter at least.

Ridiculous CC bug I encountered, that others have encountered as well: I asked Fable to review a commit. Suddenly my Fable quota for the week was at 100%, while a moment ago it was at 55%. A few days pass (1 day before the weekly reset) the quota resets back to 55%. ?!?!?!?!