alt Hacker NewsThe lean proof being correct is easy to verify, whether it proves the thing we care about is much harder.
If your code compiles, are you sure it's bug free?
Replies
jansport123 • yesterday at 4:42 PM
syntax vs semantics
The lean proof being correct is easy to verify, whether it proves the thing we care about is much harder.
If your code compiles, are you sure it's bug free?
syntax vs semantics
I'm pretty sure Mathlib has had enough human authored definitions to formalize the basic calculus necessary to state Navier-Stokes for quite some time? Some other problems admittedly need quite a bit of machinery built up to even try to say what the question is, but every undergrad learns multiple approaches to formally define everything necessary to write down a PDE.