English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Mathematical theorems are human knowledge able to be accumulated in the formof symbolic representation, and proving theorems has been consideredintelligent behavior. Based on the BHK interpretation and the Curry-Howardisomorphism, proof assistants, software capable of interacting with human forconstructing formal proofs, have been developed in the past several decades.Since proofs can be considered and expressed as programs, proof assistantssimplify and verify a proof by computationally evaluating the programcorresponding to the proof. Thanks to the transformation from logic tocomputation, it is now possible to generate or search for formal proofsdirectly in the realm of computation. Evolutionary algorithms, known to beflexible and versatile, have been successfully applied to handle a variety ofscientific and engineering problems in numerous disciplines for also severaldecades. Examining the feasibility of establishing the link betweenevolutionary algorithms, as the program generator, and proof assistants, as theproof verifier, in order to automatically find formal proofs to a given logicsentence is the primary goal of this study. In the article, we describe indetail our first, ad-hoc attempt to fully automatically prove theorems as wellas the preliminary results. Ten simple theorems from various branches ofmathematics were proven, and most of these theorems cannot be proven by usingthe tactic auto alone in Coq, the adopted proof assistant. The implication andpotential influence of this study are discussed, and the developed source codewith the obtained experimental results are released as open source.

Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants