A parser for auto-formalization in education

This project is a proof of concept for the use of a parser for auto-formalization in education. The aim was to build an easy-to-expand translation system for mathematical proofs, translating natural language proofs to machine-verifiable lean4 code, statement by statement. One example of such a statement is "Considering the different possibilities of the modulo operation, we have $q \mod 3 \in \{ 0, 1, 2 \}$.". This translation works by identifying keywords such as "have" to extract the meaning of the sentence, while other "filler" words are ignored. This allows us to write proofs in a way that is readable and feels natural, although knowledge of the keywords is very important. We managed to create a system that will allow us to easily add support for real numbers, inequalities, and justifications when they will be supported in lean4.