Is the Mizar System feasible for checking basic proofs?

75 Views Asked by At

Learning mathematics can be intimidating at times and it can be very useful to have positive feedback when writing proofs for homeworks. Is the Mizar System suitable for this sort of task? I'm not sure if it is meant for casual use like this or if it requires a substantial amount of time to input a proof. Of course, I could spend the time downloading it and reading more about it, but I figured I would ask here to see if anyone has a direct answer or general advice.