Використання AI в автоматичному доведенні математичних тверджень

Abstract

This paper examines the application of AI in automating mathematical proofs, with particular focus on three significant approaches: the Gоеdel-Prover model,Isabelle /HOL(developed by University of Cambridge) and , of course, GPT-based systems. We analyze the methodologies employed for formalizing and generating proofs, as well as the representation and construction of mathematical knowledge within these systems. Special attention is gi ven to the GоеdelProver model as a case study of successful integration between Large Language Models and the formal verification capabilities of the Lean 4 theorem proving language. Through comparative analysis, we identify the strengths and limitations of each approach, including advatages, disadvantages and opportunities for future research in AI-assisted mathematical reasoning.