Математична модель автоматичної верифікації формалізованих доказів і консервативний інтерфейс представлення в Lean

doi:10.26565/2304-6201-2026-69-03

Олександр Євдокимов Національний аерокосмічний університет «Харківський авіаційний інститут», вул. Вадима Манька, 17, Харків, Україна, 61070 https://orcid.org/0009-0008-9687-6344
Оксана Лучшева старший викладач, кафедра інженерії програмного забезпечення https://orcid.org/0000-0003-3855-2815

DOI: https://doi.org/10.26565/2304-6201-2026-69-03

Ключові слова: Lean, залежні типи, автоматична верифікація доказів, формалізована математика, консервативний інтерфейс, генеративний педагогічний модуль

Завантаження

##plugins.generic.usageStats.noStats##

Біографії авторів

Олександр Євдокимов, Національний аерокосмічний університет «Харківський авіаційний інститут», вул. Вадима Манька, 17, Харків, Україна, 61070

аспірант, кафедра математичного моделювання та штучного інтелекту

Оксана Лучшева, старший викладач, кафедра інженерії програмного забезпечення

Національний аерокосмічний університет «Харківський авіаційний інститут», вул. Вадима Манька, 17, Харків, Україна, 61070

Посилання

L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer, “The Lean Theorem Prover (System Description),” in Automated Deduction – CADE-25, vol. 9195, 2015, pp. 378–388, https://doi.org/doi: 10.1007/978-3-319-21401-6_26.

L. de Moura and S. Ullrich, “The Lean 4 Theorem Prover and Programming Language,” in Automated Deduction – CADE 28, vol. 12699, 2021, pp. 625–635, doi: 10.1007/978-3-030-79876-5_37.

The mathlib Community, “The Lean Mathematical Library,” in Proc. CPP 2020, 2020, pp. 367–381, https://doi.org/doi: 10.1145/3372885.3373824.

T. Coquand and G. Huet, “The calculus of constructions,” Inf. Comput., vol. 76, no. 2–3, pp. 95–120, 1988, doi: 10.1016/0890-5401(88)90005-3.

P. Martin-Löf, Intuitionistic Type Theory. Napoli, Italy: Bibliopolis, 1984.

P. Wadler, “Propositions as Types,” Commun. ACM, vol. 58, no. 12, pp. 75–84, 2015, https://doi.org/10.1145/2699407.

J. Avigad and P. Massot, Mathematics in Lean. Lean community tutorial, 2025. [Online]. Available: https://leanprover-community.github.io/mathematics_in_lean/

A. Thoma and P. Iannone, “Learning about Proof with the Theorem Prover LEAN: the Abundant Numbers Task,” Int. J. Res. Undergrad. Math. Educ., vol. 8, pp. 64–93, 2022, doi: 10.1007/s40753-021-00140-1.

P. Iannone and A. Thoma, “Interactive theorem provers for university mathematics: an exploratory study of students’ perceptions,” Int. J. Math. Educ. Sci. Technol., 2024, https://doi.org/doi: 10.1080/0020739X.2023.2178981.

X. K. Yan and G. Hanna, “Using the Lean interactive theorem prover in undergraduate mathematics,” Int. J. Math. Educ. Sci. Technol., 2023, https://doi.org/doi: 10.1080/0020739X.2023.2227191.

P. Massot, “Teaching Mathematics Using Lean and Controlled Natural Language,” in Leibniz Int. Proc. Inform. (LIPIcs), vol. 309, 2024, Art. no. 27, https://doi.org/doi: 10.4230/LIPIcs.ITP.2024.27.

J. Wemmenhove et al., “Waterproof: Educational Software for Learning How to Write Mathematical Proofs,” arXiv:2211.13513, 2022, https://doi.org/doi: 10.48550/arXiv.2211.13513.

O. Yevdokymov, A. Chukhray, and T. Stoliarenko, “Operationalizing the Formalizability of Mathematics Problems for Intelligent Tutoring Systems: Taxonomy, Measurement Protocol, and Educational Impact,” CEUR Workshop Proc., vol. 4164, paper 25, 2026.

A. Chukhray, D. Dvinskykh, V. Narozhnyy, and T. Stoliarenko, “Using an expression tree for adaptive learning,” in 2023 13th Int. Conf. Dependable Syst., Services Technol. (DESSERT), Athens, Greece, 2023, pp. 1–5, https://doi.org/10.1109/DESSERT61349.2023.10416497.

A. Chukhray, T. Stoliarenko, O. Yevdokymov, and V. Demyanenko, “Possibilities of using Intelligent Tutoring Systems (ITS) in Higher Mathematics Courses,” Open Inf. Comput. Integr. Technol., no. 102, pp. 92–119, 2025, https://doi.org/10.32620/oikit.2024.102.07.