Is it possible to write a program to work a math proof?

Question

given the program has all required rules and axioms. Or is there some theory making such task uncomputable?

Answer 1

You can write some rules for a program, which can then go exploring to fill in the steps in a proof. Clever programmers can build in rules to suggest which kind of steps are more likely to work at each stage. There are some well-known examples of such programs coming up with clever proofs that the person writing the program did not know about or expect.

However, high-school math is about all they have managed up till now.

Answer 2

Not impossible, but extremely difficult.

It would only do this by brute-force enumeration, i.e., it would start with the start and end points and try every possible transformation and continue onward.

One could "cheat" by incorporating all proofs known to the programmer and it would appear to do the proofs.