Towards the automatic mathematician
The authors in this paper examine recent progress in the field of neural theorem proving and their goal to create an artificial mathematician. They acknowledge the challenges that lie ahead, but highlight that even partial success in this mission could bring substantial benefits to the formal methods community and related areas such as verification, program synthesis, and natural language understanding. A survey of AI researchers conducted in 2018 estimated that machines would be capable of routinely proving mathematical theorems in top journals by the 2060s. However, the authors believe that recent breakthroughs in deep learning suggest that the development of an intelligent artificial mathematician may occur much sooner. Despite ongoing challenges, the authors are optimistic about the potential for future success in this field. For the entire collection see [Zbl 1475.68026].
- 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
- scientific article; zbMATH DE number 1882060 (Why is no real title available?)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- MPTP-motivation, implementation, first experiments
- TacticToe: learning to reason with HOL4 tactics
- A prospective on mathematics and artificial intelligence: Problem solving=Modeling+Theorem proving
- Automating formalization by statistical and semantic parsing of mathematics
- First experiments with neural translation of informal to formal mathematics
- Deep learning for math knowledge processing
- Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues
- Deepalgebra -- an outline of a program
- Mathematics by machine
- scientific article; zbMATH DE number 5629924 (Why is no real title available?)
- scientific article; zbMATH DE number 3898269 (Why is no real title available?)
- scientific article; zbMATH DE number 1782448 (Why is no real title available?)
- Deep network guided proof search
- Property invariant embedding for automated reasoning
- A study of continuous vector representations for theorem proving
- Advancing mathematics by guiding human intuition with AI
- Machine learning and the continuum hypothesis
- Solving arithmetic mathematical word problems: a review and recent advancements
- 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
- Automated proof synthesis for the minimal propositional logic with deep neural networks
- Mathematical reasoning and the computer
- Machine learning and information theory concepts towards an AI mathematician
- Generative AI and accuracy in the history of mathematics
- Large language models for mathematicians
- Considerations on approaches and metrics in automated theorem generation/finding in geometry
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)
