1. Новиков П.С. Конструктивная математическая логика с точки зрения классической. М.: Наука, 1977.
2. Колмогоров А.Н. О принципе tertium non datur // Математический сборник. 1925. Т. 32. № 4. С. 646-667. https://www.mathnet.ru/rus/sm7425.
3. Шанин Н.А. Конструктивные вещественные числа и конструктивные функциональные пространства // Труды Математического института имени В.А. Стеклова. 1962. Т. 67. С. 15-294. https://www.mathnet.ru/rus/tm1757.
4. Robinson J.A. A machine-oriented logic based on the resolution principle // Journal of the ACM. 1965. Vol. 12. No. 1. P. 23-41. DOI: 10.1145/321250.321253
5. Драгалин А.Г. Конструктивная теория доказательств и нестандартный анализ. М.: Едиториал УРСС, 2003. https://zbmath.org/1102.03003. EDN: QJMCGT
6. Paulson L.C. (Ed.). Isabelle. A generic theorem prover. Berlin-Heidelberg: Springer, 1994. DOI: 10.1007/BFb0030541
7. Harrison J. HOL Light: A tutorial introduction // Formal methods in computer-aided design. Berlin-Heidelberg: Springer, 1996. P. 265-269. DOI: 10.1007/BFb0031814
8. Wiedijk F. The seventeen provers of the world. Berlin-Heidelberg: Springer, 2006. DOI: 10.1007/11542384
9. Lenat D.B. Eurisko: A program that learns new heuristics and domain concepts: The nature of heuristics III: Program design and results // Artificial Intelligence. 1983. Vol. 21. Issues 1-2. P. 61-98. DOI: 10.1016/S0004-3702(83)80005-8
10. Urban J. MaLARea: a metasystem for automated reasoning in large theories // ESARLT: Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, German, 15th July, 2007. 2007. P. 45-58. https://ceur-ws.org/Vol-257/05_Urban.pdf.
11. Bansal K., Loos S.M., Rabe M.N., Szegedy C., Wilcox S. HOList: An environment for machine learning of higher-order theorem proving // arXiv:1904.03241 [cs.LO]. 2019. DOI: 10.48550/arXiv.1904.03241 EDN: GZEXUL
12. Piotrowski B., Urban J. ATPBOOST: Learning premise selection in binary setting with ATP feedback // Automated Reasoning. Cham: Springer, 2018. P. 566-574. DOI: 10.1007/978-3-319-94205-6_37
13. Kaliszyk C., Urban J., Michalewski H., Olšák M. Reinforcement learning of theorem proving // arXiv:1805.07563 [cs.AI]. 2018. DOI: 10.48550/arXiv.1805.07563
14. Huang D., Dhariwal P., Song D., Sutskever I. GamePad: A learning environment for theorem proving // arXiv:1806.00608 [cs.LG]. 2018. DOI: 10.48550/arXiv.1806.00608
15. Polu S., Sutskever I. Generative language modeling for automated theorem proving // arXiv:2009.03393 [cs.LG]. 2020. DOI: 10.48550/arXiv.2009.03393
16. Wu Y., Jiang A.Q., Li W., Rabe M.N., Staats C., Jamnik M., Szegedy C. Autoformalization with Large Language Models // arXiv:2205.12615 [cs.LG]. 2022. DOI: 10.48550/arXiv.2205.12615
17. Polu S., Han J.M., Zheng K., Baksys M., Babuschkin I., Sutskever I. Formal mathematics statement curriculum learning // arXiv:2202.01344 [cs.LG]. 2022. DOI: 10.48550/arXiv.2202.01344
18. Chen Wenhu, Yin Ming, Ku Max, Lu Pan, Wan Yixin, Ma Xueguang, Xu Jianyu, Wang Xinyi, Xia Tony. TheoremQA: A theorem-driven question answering dataset // Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing. Singapore: Association for Computational Linguistics, 2023. P. 7889-7901. DOI: 10.18653/v1/2023.emnlp-main.489
19. Gauthier T., Kaliszyk C., Urban J., Kumar R., Norrish M. TacticToe: learning to prove with tactics // Journal of Automated Reasoning. 2021. Vol. 65. Issue 2. P. 257-286. DOI: 10.1007/s10817-020-09580-x EDN: TBZGAH
20. Li Wenda, Yu Lei, Wu Yuhuai, Paulson L.C. IsarStep: a benchmark for high-level mathematical reasoning // arXiv:2006.09265 [cs.LO]. 2020. DOI: 10.48550/arXiv.2006.09265
21. Yang Kaiyu, Swope A.M., Gu Alex, Chalamala Rahul, Song Peiyang, Yu Shixing, Godil Saad, Prenger Ryan, Anandkumar Anima. LeanDojo: Theorem proving with retrieval-augmented language models // arXiv:2306.15626 [cs.LG]. 2023. DOI: 10.48550/arXiv.2306.15626