HackerPapers

arXiv:1610.01044cs.AI

DeepAlgebra - an outline of a program

Przemyslaw Chojecki

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
6 pages, https://przchojecki.github.io/deepalgebra/
Journal reference
DOI
Subjects
cs.AIArtificial Intelligence math.AGAlgebraic Geometry

On Hacker News

Linked by 1 identifiable commenter in 2 comments across 2 threads, from Nov 2018 to Aug 2019.

Comments linking this paper, per year.

Discussed in comments2 threads

  1. Learning to prove theorems via interacting with proof assistants 1 comment

    • Related: https://arxiv.org/abs/1610.01044 "DeepAlgebra - an outline of a program" > 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…

      carapaceView on HNParent context

  2. Logic, Explainability and the Future of Understanding 1 comment

    • If you liked that you'll like this: http://www.markability.net/ It's a walk-through of George Spencer-Brown's Laws of Form. It turns out all logic can be modeled by simple containment, and there's a complete basis (discovered by Bricken): A() = () ((A))B = AB A(AB) = A(B) One…

      carapaceView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.