ITP 2025 Overview

ITP is the leading international conference for researchers in interactive theorem proving and related areas.

Topics Covered

Proof Assistants

• Lean 4 ecosystem developments
• Coq improvements and libraries
• Isabelle/HOL automation
• New proof assistant designs

Formalization

• Large-scale mathematics formalization
• Verified algorithms and systems
• Hardware verification
• Security proofs

AI Integration

• Machine learning for premise selection
• Neural theorem provers
• Autoformalization
• AI-assisted tactic generation

Notable Formalizations

• Perfectoid spaces (completed)
• Fermat’s Last Theorem (case n=3)
• RISC-V processor verification
• Cryptographic protocol verification

Tools and Systems

• New tactics and proof methods
• IDE improvements
• Cloud-based proving
• Collaborative proof development

Community

ITP brings together mathematicians, computer scientists, and engineers working on formal methods.