This was super ambitious. Despite Godel’s incompleteness theorem, I thought it interesting to create some program which can scan through theorems or statements written in first order logic and use them to prove another theorem. It managed to show the steps for a small theorem from complex analysis. You can find the full report in this link MH4921.

The following is the preview to the report. We want to prove mathematical statements in an automated way. First, we define the predicates, then we use first order logic formulation to proceed with the proofs, i.e. sequence of statements, axioms and inferences leading to the main statement.

Here is the snapshot of the program.

You can find some of the codes in my github. Cheers!