A Mathematical Model of Automatic Verification of Formalized Proofs and a Conservative Presentation Interface over Lean. Bulletin of V.N. Karazin Kharkiv National University, series «Mathematical modeling. Information technology. Automated control systems», v. 69, p. 33–40, 30 Mar.2026.