{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T04:03:57Z","timestamp":1750565037036,"version":"3.41.0"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1109\/cec.2017.7969480","type":"proceedings-article","created":{"date-parts":[[2017,7,7]],"date-time":"2017-07-07T18:26:43Z","timestamp":1499452003000},"page":"1495-1502","source":"Crossref","is-referenced-by-count":1,"title":["Proving theorems by using evolutionary search with human involvement"],"prefix":"10.1109","author":[{"family":"Szu-Yi Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ying-ping","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"journal-title":"The Coq proofassistant","year":"0","key":"ref10"},{"journal-title":"Isabelle\/HOLA Proof Assistant for Higher-Order Logic","year":"0","author":"nipkow","key":"ref11"},{"journal-title":"HOL Interactive theorem prover","year":"0","key":"ref12"},{"journal-title":"ISABELLE","year":"0","key":"ref13"},{"journal-title":"The theory of LEGO A proof checker for the extended calculus of constructions","year":"1994","author":"pollack","key":"ref14"},{"journal-title":"The LEGO proof assistant","year":"0","key":"ref15"},{"journal-title":"The origins and motivations of univalent foundations A personal mission to develop computer proof verification to avoid mathematical mistakes","year":"2014","author":"voevodsky","key":"ref16"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1147\/rd.24.0336"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1038\/529437a"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1038\/nature16961"},{"journal-title":"The GNU Debugger","year":"0","key":"ref28"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2699407"},{"journal-title":"GDB The GNU Project Debugger","year":"0","key":"ref27"},{"journal-title":"Inst Advanced Study","article-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013","key":"ref3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1238844.1238856"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.98"},{"journal-title":"OCaml is an industrial strength programming language supporting functional imperative and object-oriented styles","year":"0","key":"ref8"},{"journal-title":"Haskell An advanced purely-functional programming language","year":"0","key":"ref7"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.20.11.584"},{"journal-title":"The LogiCal project","article-title":"The Coq proof assistant reference manual","year":"2004","key":"ref9"},{"key":"ref1","article-title":"History of constructivism in the twentieth century","author":"troelstra","year":"1991","journal-title":"Tech Rep ML-91-05"},{"journal-title":"AlphaGo","year":"0","key":"ref20"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/CEC.2016.7744352"},{"key":"ref21","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195099713.001.0001","author":"b\u00e4ck","year":"1996","journal-title":"Evolutionary Algorithms in Theory and Practice Evolution Strategies Evolutionary Programming Genetic Algorithms"},{"key":"ref24","first-page":"165","article-title":"Nouvelles approches du «théorème» de Fermat","volume":"694","author":"oesterl\u00e9","year":"1997","journal-title":"S&#x00E9 minaire Bourbaki"},{"key":"ref23","article-title":"Open problems","author":"masser","year":"1985","journal-title":"Proceedings of the Symposium on Analytic Number Theory"},{"journal-title":"Github","year":"0","key":"ref26"},{"journal-title":"Natural computing laboratory on GitHub","year":"0","key":"ref25"}],"event":{"name":"2017 IEEE Congress on Evolutionary Computation (CEC)","start":{"date-parts":[[2017,6,5]]},"location":"Donostia, San Sebasti\u00e1n, Spain","end":{"date-parts":[[2017,6,8]]}},"container-title":["2017 IEEE Congress on Evolutionary Computation (CEC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7959755\/7969277\/07969480.pdf?arnumber=7969480","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T15:22:16Z","timestamp":1750519336000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7969480\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/cec.2017.7969480","relation":{},"subject":[],"published":{"date-parts":[[2017,6]]}}}