Self-Study and Proof-Assistant Software

228 Views Asked by At

I'm not sure if this is a right question to ask or correct platform to ask. But still putting it here in case it's right thing to do. If not, please let me know I'll delete the question.

I just came across theorem-prover programming language, Lean. I'm still studying about it, so don't know complete details about it. My understanding is, it helps in confirming if the theorem proof is correct or not.

If that's true can we use it during solving proof problems during self-study? The biggest problem I face during self-studying math is I'm not always very sure if the proof answer I wrote is correct or not. Solutions from manuals or other sources not always helpful as the method I took might not be the same as given in the solution. And since we are doing self-study, getting help from other is not always possible. So, Lean kind of things might be very useful. I can write the proof in Lean & Lean can tell me if it's correct or not.

So, is Lean (or some other similar language) help in this case?

Thanks!