Towards the automatic mathematician

DOI10.1007/978-3-030-79876-5_2MaRDI QIDQ2055841zbMATH OpenOpenAlexFDO

Authors Markus Rabe, Christian Szegedy

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-79876-5_2

zbMATH Keywords

machine learningtheorem provingautomated reasoningmathematical reasoningnatural language understanding

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Formalization of mathematics in connection with theorem provers (68V20) Natural language processing (68T50) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Deep network guided proof search
• Deepalgebra -- an outline of a program
• Learning2Reason
• A promising path towards autoformalization and general artificial intelligence
• Automated proof synthesis for the minimal propositional logic with deep neural networks

Cites work

• scientific article; zbMATH DE number 1882060 (Why is no real title available?)
• A formal proof of the Kepler conjecture
• A machine-checked proof of the odd order theorem
• ATPboost: learning premise selection in binary setting with ATP feedback
• Deep network guided proof search
• Discovering governing equations from data by sparse identification of nonlinear dynamical systems
• ENIGMA: efficient learning-based inference guiding machine
• MPTP-motivation, implementation, first experiments
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• TacticToe: learning to reason with HOL4 tactics

Cited in

(24)

• Machine learning and information theory concepts towards an AI mathematician
• A prospective on mathematics and artificial intelligence: Problem solving=Modeling+Theorem proving
• Generative AI and accuracy in the history of mathematics
• Deep network guided proof search
• Property invariant embedding for automated reasoning
• Deepalgebra -- an outline of a program
• Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues
• Mathematics by machine
• A study of continuous vector representations for theorem proving
• scientific article; zbMATH DE number 5629924 (Why is no real title available?)
• Large language models for mathematicians
• Deep learning for math knowledge processing
• First experiments with neural translation of informal to formal mathematics
• Machine learning and the continuum hypothesis
• Advancing mathematics by guiding human intuition with AI
• Automating formalization by statistical and semantic parsing of mathematics
• scientific article; zbMATH DE number 3898269 (Why is no real title available?)
• Solving arithmetic mathematical word problems: a review and recent advancements
• Automated proof synthesis for the minimal propositional logic with deep neural networks
• Mathematical reasoning and the computer
• A formal proof of the expressiveness of deep learning
• A formal proof of the expressiveness of deep learning
• CoProver: a recommender system for proof construction
• scientific article; zbMATH DE number 1782448 (Why is no real title available?)

This page was built for publication: Towards the automatic mathematician

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