alt Hacker NewsThe code generation for Lean is not AFAIK verified in any way. It uses C as a portable assembler, and uses too many fancy C constructs to be compiled by CompCert C, which is the only fully verified compiler.
So you can have the strange situation of proof that the Lean code is correct, but no way of proving that the running machine code corresponds with the same program.
There is also the problem of knowing whether the microprocessor works according to its spec, and I don't think we have anything public about modern multi core processors about that.
Still, this is not a bad situation overall. If you are forced to trust the C compiler to correctly compile C, and the hardware to correctly implement the instructions in the documentation, well, you're already forced to trust both of those every day.
So this doesn't give you an absolute proof of correctness. But it does substantially reduce the size of the problem, which is now limited to (1) verifying that you actually proved what you think you did, and (2) all the stuff you were normally trusting anyway. (Some of the stuff you were trust anyway is broken, of course.) But this is a smaller problem than trusting 1,000 lines of highly-optimized CSG code written by a model we don't actually understand.