Time spent on checking proof terms

Stream: lean4

[Son Ho]

This is a curious question. Whenever I use Coq, after a proof is complete, Coq spends a fair amount of time on the Qed because it needs to check the proof term generated by the tactics. In Lean, I never witnessed this: after I reach the end of a proof, Lean manages to quickly move to the next theorem, even for reasonably big proofs. I've been quite amazed by that. So my question is: where is the magic?

Sub-question: if we use termination_by and decreasing_by clauses, after Lean has checked the proof of termination, we need to wait an amount of time which is proportional to the time spent on playing the main body of the proof (the proof without the proof of termination). Is it because Lean needs to modify and subsequently re-check the proof term to account for the termination measure?

[Mario Carneiro]

the magic is that lean doesn't do a lot of computation at the end of a proof, unlike coq

[Mario Carneiro]

the kernel does recheck the proof, but this is usually not a bottleneck

[Mario Carneiro]

to the sub-question, yes lean will do some modifications to the expression when trying to eliminate the recursion. It shouldn't be that expensive though, and I am doubtful it is (supposed to be) linear in the average case