DeepAlgebra - an outline of a program
This is an incremental proposal for researchers in formal mathematics and algebraic geometry to enhance theorem proving automation.
The paper tackles the problem of automating theorem proving in algebra and algebraic geometry by proposing a program that constructs a dictionary between automated theorem provers and LaTeX using syntactic parsers, applied to The Stacks Project repository with deep learning techniques, but no concrete results or numbers are provided.
We outline a program in the area of formalization of mathematics to automate theorem proving in algebra and algebraic geometry. We propose a construction of a dictionary between automated theorem provers and (La)TeX exploiting syntactic parsers. We describe its application to a repository of human-written facts and definitions in algebraic geometry (The Stacks Project). We use deep learning techniques.