{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:22:28Z","timestamp":1759882948419,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:00:00Z","timestamp":1759881600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:00:00Z","timestamp":1759881600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_5","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:43:28Z","timestamp":1759844608000},"page":"71-90","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Exploring Formal Math on the Blockchain: An\u00a0Explorer for Proofgold"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-6059","authenticated-orcid":false,"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1384-1613","authenticated-orcid":false,"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,8]]},"reference":[{"key":"5_CR1","unstructured":"The Lean mathematical library. CoRR abs\/1910.09336 (2019), http:\/\/arxiv.org\/abs\/1910.09336"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Ahrens, B., Matthes, R., M\u00f6rtberg, A.: From signatures to monads in UniMath. J. Autom. Reason. 63(2), 285\u2013318 (2019). https:\/\/doi.org\/10.1007\/S10817-018-9474-4, https:\/\/doi.org\/10.1007\/s10817-018-9474-4","DOI":"10.1007\/S10817-018-9474-4"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Asperti, A., Guidi, F., Coen, C.S., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: Whelp. In: Filli\u00e2tre, J., Paulin-Mohring, C., Werner, B. (eds.) Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a03839, pp. 17\u201332. Springer (2004). https:\/\/doi.org\/10.1007\/11617990_2, https:\/\/doi.org\/10.1007\/11617990_2","DOI":"10.1007\/11617990_2"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Bancerek, G., Byli\u0144ski, C., Grabowski, A., Korni\u0142owicz, A., Matuszewski, R., Naumowicz, A., P\u0105k, K.: The role of the Mizar mathematical library for interactive proof development in Mizar. J. Autom. Reason. 61(1-4), 9\u201332 (2018). https:\/\/doi.org\/10.1007\/S10817-017-9440-6, https:\/\/doi.org\/10.1007\/s10817-017-9440-6","DOI":"10.1007\/S10817-017-9440-6"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Bercic, K., Kohlhase, M., Rabe, F.: Towards a unified mathematical data infrastructure: Database and interface generation. In: Kaliszyk, C., Brady, E.C., Kohlhase, A., Coen, C.S. (eds.) Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11617, pp. 28\u201343. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_3, https:\/\/doi.org\/10.1007\/978-3-030-23250-4_3","DOI":"10.1007\/978-3-030-23250-4_3"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., Zanella-B\u00e9guelin, S.: Formal verification of smart contracts: Short paper. In: Murray, T.C., Stefan, D. (eds.) Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2016, Vienna, Austria, October 24, 2016. pp. 91\u201396. ACM (2016). https:\/\/doi.org\/10.1145\/2993600.2993611, https:\/\/doi.org\/10.1145\/2993600.2993611","DOI":"10.1145\/2993600.2993611"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Haslbeck, M.W., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09150, pp. 3\u201317. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_1, https:\/\/doi.org\/10.1007\/978-3-319-20615-8_1","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Brown, C.E., Kaliszyk, C., Gauthier, T., Urban, J.: Proofgold: Blockchain for formal methods. In: Dargaye, Z., Schneidewind, C. (eds.) 4th International Workshop on Formal Methods for Blockchains, FMBC@CAV 2022, August 11, 2022, Haifa, Israel. OASIcs, vol.\u00a0105, pp. 4:1\u20134:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/OASICS.FMBC.2022.4, https:\/\/doi.org\/10.4230\/OASIcs.FMBC.2022.4","DOI":"10.4230\/OASICS.FMBC.2022.4"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Brown, C.E., P\u0105k, K.: A tale of two set theories. In: Kaliszyk, C., Brady, E.C., Kohlhase, A., Coen, C.S. (eds.) Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11617, pp. 44\u201360. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_4, https:\/\/doi.org\/10.1007\/978-3-030-23250-4_4","DOI":"10.1007\/978-3-030-23250-4_4"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. pp. 299\u2013312. ACM (2020). https:\/\/doi.org\/10.1145\/3372885.3373830, https:\/\/doi.org\/10.1145\/3372885.3373830","DOI":"10.1145\/3372885.3373830"},{"key":"5_CR11","unstructured":"Byli\u0144ski, C.: Introduction to categories and functors. Formalized Mathematics 1(2), 409\u2013420 (1990), http:\/\/fm.mizar.org\/1990-1\/pdf1-2\/cat_1.pdf"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Corbineau, P., Kaliszyk, C.: Cooperative repositories for formal proofs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04573, pp. 221\u2013234. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73086-6_19, https:\/\/doi.org\/10.1007\/978-3-540-73086-6_19","DOI":"10.1007\/978-3-540-73086-6_19"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Desharnais, M., T\u00f3th, B., Waldmann, U., Blanchette, J., Tourret, S.: A modular formalization of superposition in Isabelle\/HOL. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia. LIPIcs, vol.\u00a0309, pp. 12:1\u201312:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2024.12, https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.12","DOI":"10.4230\/LIPICS.ITP.2024.12"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Doan, T.T.H., Thiemann, P.: A formal verification framework for tezos smart contracts based on symbolic execution. In: Kiselyov, O. (ed.) Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings. Lecture Notes in Computer Science, vol. 15194, pp. 305\u2013324. Springer (2024). https:\/\/doi.org\/10.1007\/978-981-97-8943-6_15, https:\/\/doi.org\/10.1007\/978-981-97-8943-6_15","DOI":"10.1007\/978-981-97-8943-6_15"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Furushima, H., Yamamichi, D., Shigenaka, S., Nakasho, K., Wasaki, K.: An integrated web platform for the Mizar mathematical library. In: Buzzard, K., Kutsia, T. (eds.) Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13467, pp. 141\u2013146. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_9, https:\/\/doi.org\/10.1007\/978-3-031-16681-5_9","DOI":"10.1007\/978-3-031-16681-5_9"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07998, pp. 163\u2013179. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14, https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T.T., Nguyen, Q.T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T.H.A., Tran, N.T., Trieu, T.D., Urban, J., Vu, K., Zumkeller, R.: A formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5 (2017). https:\/\/doi.org\/10.1017\/fmp.2017.1","DOI":"10.1017\/fmp.2017.1"},{"issue":"2","key":"5_CR18","first-page":"35","volume":"3","author":"M Hendriks","year":"2010","unstructured":"Hendriks, M., Kaliszyk, C., van Raamsdonk, F., Wiedijk, F.: Teaching logic using a state-of-the-art proof assistant. Acta Didactica Napocensia 3(2), 35\u201348 (June 2010)","journal-title":"Acta Didactica Napocensia"},{"key":"5_CR19","volume-title":"Introduction to higher order categorical logic","author":"J Lambek","year":"1986","unstructured":"Lambek, J., Scott, P.: Introduction to higher order categorical logic. Cambridge University Press, Cambridge, UK (1986)"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Nawrocki, W., Ayers, E.W., Ebner, G.: An extensible user interface for Lean 4. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bia\u0142ystok, Poland. LIPIcs, vol.\u00a0268, pp. 24:1\u201324:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.24, https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.24","DOI":"10.4230\/LIPICS.ITP.2023.24"},{"key":"5_CR21","unstructured":"Stark, E.W.: Category theory with adjunctions and limits. Arch. Formal Proofs 2016 (2016), https:\/\/www.isa-afp.org\/entries\/Category3.shtml"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Tomaszuk, D., Szeremeta, \u0141., Korni\u0142owicz, A.: MMLKG: Knowledge graph for mathematical definitions, statements and proofs. Sci Data 10(791) (2023), https:\/\/doi.org\/10.1038\/s41597-023-02681-3","DOI":"10.1038\/s41597-023-02681-3"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Vezzosi, A., M\u00f6rtberg, A., Abel, A.: Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang. 3(ICFP), 87:1\u201387:29 (2019). https:\/\/doi.org\/10.1145\/3341691, https:\/\/doi.org\/10.1145\/3341691","DOI":"10.1145\/3341691"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Wiedijk, F.: Introduction. In: Wiedijk, F. (ed.) The Seventeen Provers of the World, Foreword by Dana S. Scott, Lecture Notes in Computer Science, vol.\u00a03600, pp.\u00a01\u20139. Springer (2006). https:\/\/doi.org\/10.1007\/11542384_1, https:\/\/doi.org\/10.1007\/11542384_1","DOI":"10.1007\/11542384_1"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07021-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:43:31Z","timestamp":1759844611000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,8]]},"ISBN":["9783032070203","9783032070210"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,8]]},"assertion":[{"value":"8 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}