There are plenty of challenges writing an automated theorem prover. They will come under the blindingly obvious but I just wanted to pad out these pages a little.

A human proving a theorem would take it as read that 2 is a prime, or that between any two integers there are a finite number of other integers. An automated theorem prover has either to have such statements built in, or be able to prove them itself as needed.

As nice as an automated theorem prover managing to prove a wanted theorem is, it’s more important it doesn’t prove what it shouldn’t. So more important not to prove 2 + 2 = 5 than to prove 2 + 2 = 4. You’re going to have plenty of test cases, and not all happy path test cases at that.

An automated theorem prover is likely to be computationally demanding in terms of time and memory. JITs are clever, and multiple threads will speed things up, but code optimisation is important. The most significant optimisations for me are those which change the algorithms used. Knuth is fundamental. I regard computer programming as much of an Art as sculpture or painting.