Interactive Theorem Proving (conference)

This article may rely excessively on sources too closely associated with the subject, potentially preventing the article from being verifiable and neutral. Please help improve it by replacing them with more appropriate citations to reliable, independent sources. (January 2025) (Learn how and when to remove this message)

Interactive Theorem Proving (ITP) is an annual international academic conference on the topic of automated theorem proving, proof assistants and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics.

ITP brings together the communities using many systems based on higher-order logic such as ACL2, Coq, Mizar, HOL, Isabelle, Lean, NuPRL, PVS, and Twelf. Individual workshops or meetings devoted to individual systems are usually held concurrently with the conference.

Together with CADE and TABLEAUX, ITP is usually one of the three main conferences of the International Joint Conference on Automated Reasoning (IJCAR) whenever it convenes,