MaProS

This project is the implementation of work from my Master thesis at UCLouvain. This is still work in progress and is not a final version of the work. The main goal is to show a proof of concept of a system that would allow a user to write a mathematical proof in a close to natural language manner. Such proof would then be translated in Lean3 to be verified.

This repository contains the frontend part of the system. This project was bootstrapped with Create React App.

Instructions are available for

External sources

  • The proof for the sandiwch theorem available at this link is used for testing.
  • The project react-mathquill is used to render math formulas.
  • react-bootstrap framework is used.