Математична модель автоматичної верифікації формалізованих доказів і консервативний інтерфейс представлення в Lean
DOI:
https://doi.org/10.26565/2304-6201-2026-69-03Ключові слова:
Lean, залежні типи, автоматична верифікація доказів, формалізована математика, консервативний інтерфейс, генеративний педагогічний модульПосилання
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.
