A Lean program that compiles proves what it states. The question is whether the program states what we think it does. If I recall, this program is 12 million lines long. Mathlib is not perfect, and it's not hard at all to have a Lean statement that isn't what you think it is.
So my question is whether people have actually checked that the generated program, all 12 million lines of it, has the statements that are expected.
So my question is whether people have actually checked that the generated program, all 12 million lines of it, has the statements that are expected.