I am learning Logic and set theory, in the process I have made some formal proofs, but this is tedious with the traditional tools. Now, I am wondering if there exists some software or something like a programming language where such formal proofs can be done. So it would be possible to create a datebase of formal proofs.
Thank you so much.