A.P. Khalov1, O.M. Ataeva2, N.P. Tuchkova3

1–3 FRC CSC RAS (Moscow, Russia)
1 Institute of Physics and Technology (National Research University) (Moscow, Russia)
1 khalov.a@phystech.edu, 2 oataeva@frccsc.ru, 3 ntuchkova@frccsc.ru

Problem Statement. This work aims to investigate the problem of verifying the quality of information generated by large language models in response to user queries regarding the validity of mathematical statements.

Objective. Implement an approach to constructing formal mathematical proofs in which large language models utilize the structured SciLib knowledge graph–built upon the MathLib formal mathematics library–thereby ensuring transparency in content delivery.

Results. The results demonstrate that utilizing the explicit structure of mathematical knowledge, as implemented in the SciLib graph, provides a more interpretable and reliable example of the interaction between theorem-proving systems and large language models.

Practical Significance. The proposed approach requires no additional training and is compatible with various neural-network-based proof systems, while the SciLib knowledge graph can be integrated into existing formal proof generation pipelines.

Khalov A.P., Ataeva O.M., Tuchkova N.P. Explaining formal mathematical proofs using large language models and the SciLib knowledge graph // Highly Available Systems. 2026. V. 22. № 3. P. 55−70. DOI: https://doi.org/10.18127/j20729472-202603-06

1. de Moura L., Ullrich S. The Lean 4 theorem prover and programming language. Proceedings of the 28th International Conference on Automated Deduction (CADE). Springer. 2021.
2. Howard W.A. The formulae-as-types notion of construction. To H.B. Curry: Essays on Combinatory Logic. Lambda Calculus and Formalism. Academic Press. 1980. P. 479–490.
3. Wadler P. Propositions as types. Communications of the ACM. 2015. V. 58. № 12. P. 75–84.
4. Martin-Löf P. Intuitionistic Type Theory. Naples: Bibliopolis. 1984.
5. The mathlib Community. The Lean mathematical library. arXiv preprint arXiv:1910.09336. 2020.
6. Yin Z., Song D., Xiong H., Yu D., Chen J. et al. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801. 2025.
7. Wang H., Liu Z., Lin X., Liu J., Sung F. et al. Kimina-Prover preview: Towards large formal reasoning models with reinforcement lear­ning. arXiv preprint arXiv:2504.11354. 2025.
8. ByteDance Seed AI4Math. Seed-Prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726. 2025.
9. Ataeva O.M., Khalov A.P., Tuchkova N.P. Multi-Level Knowledge Graph for Formal Mathematics. Lobachevskii Journal of Mathematics. 2026. V. 47. № 6. P. 2725–2739 https://doi.org/10.1134/S1995080226618990
10. Ataeva O.M., Tuchkova N.P. Materializaciya ontologii nauchny`x danny`x cherez semanticheskij graf biblioteki SciLibRu. Programmirovanie. 2026. № 5. S. 17–36. https://doi.org/10.7868/S3034584726050039 (in Russian).
11. Zheng K., Han J. M., Polu S. miniF2F: A cross-system benchmark for formal Olympiad-level mathematics. International Conference on Learning Representations (ICLR). 2022.
12. The Harmonic Team. Aristotle: IMO-level automated theorem proving. arXiv preprint arXiv:2510.01346. 2025.
13. Lewis P., Perez E., Piktus A., Petroni F., Karpukhin V., Goyal N., Küttler H., Lewis M., Yih W., Rocktäschel T. et al. Retrieval-augmented generation for knowledge-intensive NLP tasks. Advances in Neural Information Processing Systems. 2020. V. 33. P. 9459–9474.
14. Ataeva O.M., Tuchkova N.P. Orkestraciya metodov analiza nauchny`x danny`x v processax recenzirovaniya. E`lektronny`e biblioteki. 2026. T. 29. Vy`p. 3. S. 655–680. https://doi.org/10.26907/1562-5419-2026-29-3-655-680 (in Russian).
15. Khalov A.P., Ataeva O.M., Tuchkova N.P. Creating a multimodal dataset for the SciLibRu semantic library using a language model. Pattern Recognition and Image Analysis. 2026. V. 36. № 2. P. 665–677. https://doi.org/10.1134/S1054661826700471
16. frenzymath/jixia: A static analysis tool for Lean 4. https://github.com/frenzymath/jixia. GitHub repository; Apache-2.0 license.
17. Hsiang R., Adkisson W., George R.J., Anandkumar A. LeanDojo-v2: A comprehensive library for AI-assisted theorem proving in Lean. NeurIPS 2025 Workshop on MATH-AI. 2025.
18. Hu L., Qin S., Liao Z., Guo Q., Wan L., Feng W., Liu Y. CoLT: Teaching multi-modal models to think with chain of latent thoughts. arXiv preprint arXiv:2606.31986. 2026. https://doi.org/10.48550/arXiv.2606.31986
19. Chen M. et al. Evaluating Large Language Models Trained on Code. arXiv 2021. https://arxiv.org/pdf/2107.03374.
20. Wilcoxon F. Individual comparisons by ranking methods. Biometrics Bulletin. 1945. V. 1. № 6. P. 80–83.