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.
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.
Since Lean can emit LLVM it might be more achievable to reach performant assembly without going via C. All sorts of interesting work in progress.
https://dl.acm.org/doi/10.1145/3192366.3192377
(I am rate limited to ~5 comments a day so not replying for ages is just a function of the HN gods on Mt Sunnyvale.)
It is the quantum effects that occur at tiny geometries that make this hard, but every chip you buy has passed extensive variation.
To account for individual variation and random glitches there are other techniques, like triple modular redundancy or lockstep processors. Or for less stringent software, just computing it twice in different cores and memory blocks.
To get the feel of this it might help to start with a simpler example: If you declare a function in ordinary old Java with return type int, the Java compiler will complain unless every path through that function returns either an int or something that can be converted to it (or throws). Lean is similar but uses a much more powerful type system called dependent types, which gives you extreme control over the values that are permitted in a type: For example, in Lean it's possible to define a type that consists of just the even integers, or even just the prime numbers. If you define such a PrimeNumber type, and then declare a function that returns a PrimeNumber, the Lean compiler will complain if the function could ever return a number that is not prime. IOW, if your function compiles with no errors, it is proven to always return a prime number.
I expect that OP's code defines a function named something like intersect(), and which takes 2 arguments of a type named something like Mesh, and returns not simply another Mesh but in fact a more complicated type: specifically, a Mesh that is somehow constrained to be a sub-mesh of each of the first and second arguments. Since mesh intersection is deterministic, I expect that this more complicated type will turn out to be inhabited by just a single value (mesh) -- similar to a type FortyTwo whose only value value is the integer 42. (I'm assuming here that a mesh can only be represented in one canonical way; this might not be true.) Then, Lean will complain at compile time if there exists any conceivable pair of input meshes for which the function would construct the wrong intersection.