在計算機科學和數理邏輯中，證明助手或交互式定理檢驗器是一種軟件工具，通過人機協作來協助開發形式證明。這涉及到某種交互式證明編輯器，或其他界面，人類可以用它來指導搜索證明，其細節存儲在計算機中，并由計算機提供一些步驟。系統比較ACL2--一種編程語言，一種一階邏輯理論，以及博耶-摩爾傳統的定理驗證器（有交互式和自動模式）。Coq--允許表達數學斷言，機械地檢查這些斷言的證明，幫助尋找形式證明，并從其形式規范的構造證明中提取認證程序。HOL定理驗證器--最終由LCF定理驗證器衍生的工具系列。在這些系統中，邏輯核心是其編程語言的一個庫。定理代表語言的新元素，只能通過保證邏輯正確性的策略引入。策略組合使用戶能夠在與系統相對較少的互動中產生重要的證明。這個家族的成員包括：HOL4-主要的后裔，仍在積極開發中。支持MoscowML和Poly/ML。HOLLight-一個蓬勃發展的極簡主義分叉，基于OCML。ProofPower-曾經是專有的，然后又回到了開放源碼。基于StandardML。IMPS,AnInteractiveMathematicalProofSystemIsabelle是一個交互式定理檢驗器，是HOL的繼承者。主要代碼庫是BSD許可的，但Isabelle發行版捆綁了許多不同許可的附加工具。Jape-基于Java。LeanLEGOMatita-基于歸納構造微積分的輕型系統。

MINLOG-基于一階最小邏輯的證明助手。Mizar-基于一階邏輯的證明助手，采用自然演繹風格，以及Tarski-Grothendieck集合理論。PhoX-基于高階邏輯的證明助手，是eXtensible。PrototypeVerificationSystem(PVS)-基于高階邏輯的證明語言和系統。TPS和ETPS-同樣基于簡單類型的lambdacalculus的交互式定理證明器，但基于邏輯理論的獨立表述和獨立實現。TypelabYarrow定理證明器博物館是一個保護定理證明器系統來源的倡議，以備將來分析，因為它們是重要的文化/科學文物。它擁有上面提到的許多系統的來源。

一個流行的證明助手的前端是基于Emacs的ProofGeneral，由愛丁堡大學開發。Coq包括CoqIDE，它是基于OCaml/Gtk的。Isabelle包括Isabelle/jEdit，它是基于jEdit和Isabelle/Scala基礎設施的面向文檔的證明處理。