関連した問題に、自動証明検証と、証明のコンピュータによる支援がある。定理の証明の正当性を検証するには、証明の各段階を原始再帰関数やプログラムで検証できる必要があり、そうすることで問題は常に決定可能となる。
自動定理証明で生成される証明は長大なものとなることが多く、証明の圧縮という問題が重要となり、様々な技法が考案されている。
対話型定理証明機では人間のユーザーがシステムにヒントを与える必要がある。自動化の度合いによっては、証明機が単なる証明検証機的なものとなってユーザーが提供した形式的証明を検証するだけの場合もあるし、大部分の証明を自動的に行う場合もある。対話型証明機は様々なタスクに使えるが、完全自動システムは長期にわたって人間の数学者がてこずってきた困難な問題を証明してきた。しかし、そのような成功例は稀で、一般に困難な問題を解くには熟練したユーザーの補助が必要である。
定理証明とそれ以外の区別の観点として、公理から出発して推論規則に従って推論を行い、いわゆる証明を行うものを定理証明と呼ぶ。モデル検査などのそれ以外の技術では、考えられる全ての状態を列挙するようなものである（モデル検査の実装ではもう少し賢さが必要であるが、それで力づくの手法でなくなるわけではない）。
モデル検査的手法を推論規則として利用するハイブリッド型の定理証明システムも存在する。また、特定の定理を証明するために書かれたプログラムも存在し、プログラムがある結果を返して終了したときに定理が真であることが証明される。そのようなプログラムの好例として四色定理の計算機支援証明がある。人間の手では証明できなかった問題を証明したことで物議をかもしたそのプログラムは、非常に複雑で検証不可能と言われた。他の例として重力付き四目並べゲームで先手が必ず勝つことを証明したことが挙げられる。
産業への応用.
一階述語論理の定理証明.
一階述語論理の定理証明は自動定理証明の中でも最も研究が進んでいる。この論理は適度に自然で直感的な方法で様々な問題を記述できる程度に表現豊かである。一方、半決定的で健全で完全な計算方法が開発されており、完全自動システムを構築することが可能である。さらに表現力のある論理（高階述語論理や様相論理）は、さらに様々な問題を記述可能だが、それらの定理証明は一階述語論理ほど開発が進んでいない。