DeepAlgebra - an outline of a program
Przemyslaw Chojecki

TL;DR
DeepAlgebra proposes a formalization framework using deep learning to connect automated theorem proving with LaTeX, aiming to automate algebraic geometry proofs by leveraging a repository of human knowledge.
Contribution
It introduces a novel approach combining deep learning, syntactic parsing, and formalization to enhance automated theorem proving in algebraic geometry.
Findings
Successful integration with The Stacks Project repository
Effective use of deep learning for syntactic parsing
Potential for automating algebraic geometry proofs
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics, Computing, and Information Processing · Semantic Web and Ontologies · Logic, programming, and type systems
