В роботі досліджено застосування ШІ в автоматичному доведенні математичних тверджень, детально розглянуто одну з найновіших та найуспішніших моделей - Gоеdel-Prover, розглянуто системи на основі GPT та Isabelle/HOL(створену у Кембріджському університеті). Проаналізовано методи формалізації та генерування доведень, а також представлення та побудову доведень математичних знань у цих системах. Особлива увага приділяється моделі Gоеdel-Prover як прикладу успішної інтеграції великих мовних моделей із можливостями формальної верифікації мови доведення теорем Lean 4. Через порівняльний аналіз визначено сильні сторони та обмеження кожного підходу, підкреслено переваги, недоліки та можливості для подальших досліджень у сфері математичного міркування за допомогою ШІ.

USE OF AI IN AUTOMATED THEOREM PROVING

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 given to the Gоеdel-Prover 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.