Comment by notrealyme123

I get the feeling a lot of people propose that we can write a verifier for every proof in lean.

Can someone tell me in simple terms why this doesn't conflict with the incompleteness theorems?

edit: thanks for the responses, i feel slightly less dumb now