Skip to main content
added 760 characters in body
Source Link
Tadashi
  • 1.6k
  • 3
  • 23
  • 29

A pre-print by Li-An Yang, Jui-Bin Liu, Chao-Hong Chen and Ying-ping Chen was submitted to arXiv last month (24 Feb) giving some preliminary results of an ad-hoc evolutionary algorithm used to prove some simple theorems within the Coq proof assistant: Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants

The paper also discuss some possible future work within this context and the code used was released as open-source at GitHub.

Update (04/26/2019):

Found today in a NewScientist article about the Deepmath project, a Google project seeking to improve automated theorem proving using deep learning and other machine learning techniques. In particular, they made a software named DeepHOL that is a deep reinforcement learning driven automated theorem prover (1).

(1): Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)

A pre-print by Li-An Yang, Jui-Bin Liu, Chao-Hong Chen and Ying-ping Chen was submitted to arXiv last month (24 Feb) giving some preliminary results of an ad-hoc evolutionary algorithm used to prove some simple theorems within the Coq proof assistant: Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants

The paper also discuss some possible future work within this context and the code used was released as open-source at GitHub.

A pre-print by Li-An Yang, Jui-Bin Liu, Chao-Hong Chen and Ying-ping Chen was submitted to arXiv last month (24 Feb) giving some preliminary results of an ad-hoc evolutionary algorithm used to prove some simple theorems within the Coq proof assistant: Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants

The paper also discuss some possible future work within this context and the code used was released as open-source at GitHub.

Update (04/26/2019):

Found today in a NewScientist article about the Deepmath project, a Google project seeking to improve automated theorem proving using deep learning and other machine learning techniques. In particular, they made a software named DeepHOL that is a deep reinforcement learning driven automated theorem prover (1).

(1): Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)

Source Link
Tadashi
  • 1.6k
  • 3
  • 23
  • 29

A pre-print by Li-An Yang, Jui-Bin Liu, Chao-Hong Chen and Ying-ping Chen was submitted to arXiv last month (24 Feb) giving some preliminary results of an ad-hoc evolutionary algorithm used to prove some simple theorems within the Coq proof assistant: Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants

The paper also discuss some possible future work within this context and the code used was released as open-source at GitHub.