Syntactic Similarity in human-oriented ATP

Abstract

Automated theorem proving (ATP) has long been a significant field in computer science, aiming to develop algorithms for finding formal proofs automatically. With the advent of proof assistants in mathematical research and, more generally, formal methods, these systems will become increasingly relevant for mathematicans, too. Over the years, researchers have explored various approaches to tackle the inherent challenges of ATP, resulting in two paradigms being heavily researched currently: Satisfiability Modulo Theories (SMT) solving and Machine Learning (ML)....