Lean + mathlib a modern interactive theorem prover with a growing standard library; widely used for formalizing real mathematics and increasingly integrated with AI tools
Coq a mature proof assistant based on constructive type theory; used for certified software (e.g. CompCert) and foundational mathematics
Z3 (SMT Solver) a high-performance satisfiability modulo theories solver; used in program analysis, formal verification, and backend automation in proof systems
Homotopy Type Theory (HoTT) a new foundation for mathematics using higher-dimensional types; encodes structure-sensitive equality via paths and supports univalent reasoning
Metamath an ultra-minimal formal system for expressing all of mathematics using explicit substitution; emphasizes kernel transparency and syntactic traceability
Lean-GPT / TheoremTactic AI-driven tools for formal proof suggestion and tactic synthesis; integrate language models with proof assistants to assist and accelerate formalization