USING LEAN PROGRAMMING LANGUAGE TO CHECK INCONSISTENCY IN MATHEMATICAL PROBLEMS IN THE EDUCATIONAL RECOMMENDATION SYSTEM

Abstract

This article describes the problem of ensuring the quality of mathematics learning in the conditions of the growing popularity of self-study. An approach based on the Lean functional programming language is proposed, which enables automatic checking for the accuracy and consistency of the data in a mathematical problem and the solution of this problem. This approach is implemented in the recommendation system that is designed for solving mathematical problems, with an interface for interaction and training the users. The created subsystem based on the Lean language can identify potential errors and inconsistencies in the conditions of the task, as well as the contribution to the correct answer of the problem.

The Lean programming language was primarily designed to serve as an efficient assistant in theorem proving, which is why this language was primarily chosen.

The Lean verification subsystem was developed by adding axioms and theorems from planimetry, which allowed the integration with the other created system modules and also allowed to perform the data consistency checks. To illustrate the potential of Lean, several examples of problems are used to demonstrate the advantages of language in ensuring the accuracy of solutions and detecting errors in mathematical problems.

In the conclusions of the article, it is emphasized that Lean effectively complements the recommendation system for solving simple planimetric problems, providing not only the verification for the inconsistency of the conditions of the problem but also the correctness of the final solutions. In addition, certain defects in the language are highlighted, which complicates its use and requires further research and development to optimize the subsystem. Compared to other approaches, such as the use of ontologies in Protégé, Lean provides significant advantages in the flexibility of defining mathematical models and performing non-trivial proofs, making Lean a powerful tool to support quality mathematics learning.