A Mathematical Model of Automatic Verification of Formalized Proofs and a Conservative Presentation Interface over Lean

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

Oleksandr Yevdokymov National Aerospace University “Kharkiv Aviation Institute”, Vadym Manko St., 17, Kharkiv, Ukraine, 61070 https://orcid.org/0009-0008-9687-6344
Oksana Luchsheva Senior Lecturer, Department of Software Engineering https://orcid.org/0000-0003-3855-2815

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

Keywords: Lean, dependent types, automatic proof verification, formalized mathematics, conservative interface, generative pedagogical module

Downloads

Download data is not yet available.

Author Biographies

Oleksandr Yevdokymov, National Aerospace University “Kharkiv Aviation Institute”, Vadym Manko St., 17, Kharkiv, Ukraine, 61070

PhD Student, Department of Mathematical Modeling and Artificial Intelligence

Oksana Luchsheva, Senior Lecturer, Department of Software Engineering

National Aerospace University “Kharkiv Aviation Institute”, Vadym Manko St., 17, Kharkiv, Ukraine, 61070

References

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.