A parser for auto-formalization in education

Files

Supervisors: Glineur, François
Faculty: Ecole polytechnique de Louvain
Degree label: Master [120] : ingénieur civil en informatique, à finalité spécialisée
Abstract: 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.

d’Oultremont, A. (2022). A parser for auto-formalization in education. https://dial-mem.test.bib.ucl.ac.be/handle/2078.2/31432