5

Not in such straight forward way as described, but neural networks are successfully applied to guide the search of proof. There are automated theorem provers. What they do look roughly like this: Get the mathematical statement Apply one of the known mathematical equivalence transformations (theorems, axioms, etc) Check, if the resulting statement is ...


5

Your idea may be feasible in general, but a neural network is probably the wrong high level tool to use to explore this problem. A neural network's strength is in finding internal representations that allow for a highly nonlinear solution when mapping inputs to outputs. When we train a neural network, those mappings are learned statistically through ...


4

Artificial Intelligence for Theorem Proving is an active research area as witnessed by the existence of the AITP conference and of many publications on the topic. Some papers are mentioned in this thread: https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303. I haven't read these papers myself, so I cannot point you to a paper using ...


3

There are programming languages that allow you to verify a proof by induction. For example, I used Coq, but I'm sure there are also others.


2

It's possible, but probably not a good idea. Logical proof is one of the oldest areas of AI, and there are purpose-built techniques that don't need to be trained, and that are more reliable than a neural-network approach would be, since they don't rely on statistical reasoning, and instead use the mathematician's friend: deductive reasoning. The main field ...


2

This is an active research topic. Consider reading J.Pitrat's Artificial Beings, the conscience of a conscious machine book This Understanding machine learning book old Lenat's papers on Eurisko. and recent papers such as Learning Structured Embeddings of Knowledge Bases and several others in Artificial Intelligence Journal about the MILEPOST GCC and ...


2

Arguably we have had this since 1957, with the General Problem Solver. However, it is a thorny problem, and like so much in AI, it works fine in toy domains (like the Towers of Hanoi problem), but fails in real life, as real life is too complex for it to cope. There is a list of solvers (the category of programs dealing with this issue) on Wikipedia. As of ...


2

There are two ways to look at the problem, one in terms of logic and the other in terms of psychology. To get any -start- on automation of mathematics, you need to formalize the part you want. It has only been since the early part of the 20th c that most day to day math had been formalized with logic and set theory. And even though Gödel's incompleteness ...


1

It is possible for some classes of problems. For instance, WolframAlpha can generate an induction proof to the problem posed in the question. According to the author of this proof generator, he built a library of pattern-matched proofs to generate the proofs. More details about his approach can be find in his write-up about the problem. Other alternative (...


1

I can see several challenges, and the list below is not exhaustive: i. The main problem is how to model a problem of translating a language test into a formal language. It will probably be something like the automatic translators, but with some guarantees that the proof semantics will be preserved. If you are more interested in this path, I recommend ...


1

Yes. Some good examples of this are Lipson's work using evolutionary models, and Wu & Tegmark's work on a theory-based life-long learner, and Iten et al.'s work with deep neural networks. There are many, many, other research papers in this area, and there is a lot more work that is ongoing. The endgame for a lot of this work is the hope that we can ...


1

I've published an article with the corresponding new method based on the generative grammars of first-order theories: Thoughts on generative grammars and their use in automated theorem proving based on neural networks This approach allows not to use previous data but to generate it as much as it's needed in machine learning. In the article, you may find ...


Only top voted, non community-wiki answers of a minimum length are eligible