Deepalgebra -- an outline of a program

DOI10.1007/978-3-319-62075-6_1MaRDI QIDQ2364671zbMATH OpenOpenAlexFDO

Authors Przemyslaw Chojecki

Publication date 21 July 2017

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

Mathematics Subject Classification ID

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

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.

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

Cites work

• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• A machine-checked proof of the odd order theorem
• MizAR 40 for Mizar 40
• Mizar: state-of-the-art and beyond
• Recycling proof patterns in Coq: case studies
• System description: E 1.8
• Theorem proving in large formal mathematics as an emerging AI field

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

Describes a project that uses

Uses Software

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

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)