{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:36:08Z","timestamp":1761510968136},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,2]]},"DOI":"10.1007\/s10817-012-9268-z","type":"journal-article","created":{"date-parts":[[2012,10,31]],"date-time":"2012-10-31T15:17:19Z","timestamp":1351696639000},"page":"119-121","source":"Crossref","is-referenced-by-count":12,"title":["Formal Mathematics for Mathematicians"],"prefix":"10.1007","volume":"50","author":[{"given":"Andrzej","family":"Trybulec","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"Kornilowicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Naumowicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krystyna","family":"Kuperberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,11,1]]},"reference":[{"key":"9268_CR1","doi-asserted-by":"crossref","unstructured":"Autexier, S. et al. (eds.): Intelligent Computer Mathematics. LNAI 6167. Springer (2010)","DOI":"10.1007\/978-3-642-14128-7"},{"key":"9268_CR2","doi-asserted-by":"crossref","unstructured":"Beringer, L., Felty, A. (eds.): Interactive Theorem Proving\u2014Third International Conference. LNCS 7406. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8"},{"key":"9268_CR3","doi-asserted-by":"crossref","unstructured":"Davenport, J., et al. (eds.): Intelligent Computer Mathematics. LNAI 6824. Springer (2011)","DOI":"10.1007\/978-3-642-22673-1"},{"issue":"11","key":"9268_CR4","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2014the four color theorem. Not. Am. Math. Soc. 55(11), 1382\u20131393 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"11","key":"9268_CR5","first-page":"1370","volume":"55","author":"TC Hales","year":"2008","unstructured":"Hales, T.C.: Formal proof. Not. Am. Math. Soc. 55(11), 1370\u20131380 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"11","key":"9268_CR6","first-page":"1395","volume":"55","author":"J Harrison","year":"2008","unstructured":"Harrison, J.: Formal proof\u2014theory and practice. Not. Am. Math. Soc. 55(11), 1395\u20131406 (2008)","journal-title":"Not. Am. Math. Soc."},{"key":"9268_CR7","doi-asserted-by":"crossref","unstructured":"Jeuring, J., et al. (eds.): Intelligent Computer Mathematics. LNAI 7362. Springer (2012)","DOI":"10.1007\/978-3-642-31374-5"},{"key":"9268_CR8","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Paulson, L.C. (eds.): Interactive Theorem Proving, First International Conference. LNCS 6172. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5"},{"key":"9268_CR9","doi-asserted-by":"crossref","unstructured":"van Eekelen, M.C.J.D., et al. (eds.): Interactive Theorem Proving\u2014Second International Conference. LNCS 6898. Springer (2011)","DOI":"10.1007\/978-3-642-22863-6"},{"issue":"11","key":"9268_CR10","first-page":"1408","volume":"55","author":"F Wiedijk","year":"2008","unstructured":"Wiedijk, F.: Formal Proof\u2014Getting Started. Not. Am. Math. Soc. 55(11), 1408\u20131414 (2008)","journal-title":"Not. Am. Math. Soc."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/s10817-012-9268-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,5]],"date-time":"2019-07-05T00:15:25Z","timestamp":1562285725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9268-z"}},"subtitle":["Foreward to the Special Issue"],"short-title":[],"issued":{"date-parts":[[2012,11,1]]},"references-count":10,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["9268"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9268-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11,1]]}}}