Deepalgebra -- an outline of a program

DOI10.1007/978-3-319-62075-6_1zbMATH Open1367.68247arXiv1610.01044OpenAlexW2529124776MaRDI QIDQ2364671FDOQ2364671

Authors: Przemyslaw Chojecki 

Publication date: 21 July 2017

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.

Full work available at URL: https://arxiv.org/abs/1610.01044

Recommendations

• Towards the automatic mathematician
• Deep network guided proof search
• Formalized proof, computation, and the construction problem in algebraic geometry
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Learning-assisted theorem proving with millions of lemmas

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to algebraic geometry (14-04)

Cites Work

• MizAR 40 for Mizar 40
• Mizar: state-of-the-art and beyond
• System description: E 1.8
• Title not available (Why is that?)
• Theorem proving in large formal mathematics as an emerging AI field
• Recycling proof patterns in Coq: case studies
• A machine-checked proof of the odd order theorem

Cited In (7)

• Deep network guided proof search
• Liquid tensor experiment
• Towards the automatic mathematician
• Automating formalization by statistical and semantic parsing of mathematics
• ML4PG in computer algebra verification
• Liquid tensor experiment
• Formalized proof, computation, and the construction problem in algebraic geometry

Uses Software

• Coq
• Mizar
• E Theorem Prover
• DeepMath
• CoqHammer

This page was built for publication: Deepalgebra -- an outline of a program

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2364671)