Proof of concept of an interactive theorem prover system using natural language input

This work presents a proof of concept for a mathematical proof system that would allow users to write in a close to natural language while generating proofs that are machine verifiable. The main objective is to assess the feasibility and features of such a project and explore promising leads to this end. The current implementation is a web application written in Python/Javascript with backend in Django and frontend in React. It constructs and verifies proofs with Lean, an interactive theorem prover. Natural language processing is made by simple pattern matching. The current implementation is still somehow limited but allows to envision a more advanced system. The last chapter develops possible ideas to further improve and extend the current proof of concept.