Comment by pvillano

Do lean poofs need to be manually reviewed?

Or is it as long as you formalize your theorem correctly, a valid lean program is an academically useful proof?

Are there any minimal examples of programs which claim to prove the thing without actually proving the thing in a meaningful way?