{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T13:15:16Z","timestamp":1765372516548,"version":"3.46.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,13]]},"DOI":"10.1145\/3761668.3761673","type":"proceedings-article","created":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T07:46:32Z","timestamp":1765352792000},"page":"23-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of the Equivalence Between Dedekind's Fundamental Theorem and the Supremum Theorem Based on Axiomatic Set Theory"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-2261-2676","authenticated-orcid":false,"given":"Ce","family":"Zhang","sequence":"first","affiliation":[{"name":"Beijing University of Posts and Telecommunications, School of Electronic Engineering, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3832-2748","authenticated-orcid":false,"given":"Wensheng","family":"Yu","sequence":"additional","affiliation":[{"name":"Beijing University of Posts and Telecommunications, School of Electronic Engineering, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,12,9]]},"reference":[{"key":"e_1_3_3_1_1_2","volume-title":"Principles of mathematical analysis[J]","author":"Rudin W.","year":"2021","unstructured":"Rudin W. Principles of mathematical analysis[J]. 2021."},{"key":"e_1_3_3_1_2_2","volume-title":"Analysis[M]","author":"Tao T.","year":"2006","unstructured":"Tao T. Analysis[M]. New Delhi, India: Hindustan Book Agency, 2006."},{"key":"e_1_3_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1090\/chel\/376"},{"key":"e_1_3_3_1_4_2","volume-title":"Introductory real analysis[M]","author":"Dangello F","year":"2000","unstructured":"Dangello F, Seyfried M. Introductory real analysis[M]. Boston: Houghton Mifflin, 2000."},{"issue":"6","key":"e_1_3_3_1_5_2","first-page":"681","article-title":"The mechanization of mathematics[J]","volume":"65","author":"Avigad J","year":"2018","unstructured":"Avigad J. The mechanization of mathematics[J]. Notices of the AMS, 2018, 65(6): 681-90.","journal-title":"Notices of the AMS"},{"key":"e_1_3_3_1_6_2","volume-title":"A machine-checked proof of the odd order theorem[C]\/\/International conference on interactive theorem proving","author":"Gonthier G","year":"2013","unstructured":"Gonthier G, Asperti A, Avigad J, et al. A machine-checked proof of the odd order theorem[C]\/\/International conference on interactive theorem proving. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013: 163-179."},{"key":"e_1_3_3_1_7_2","volume-title":"Pi","author":"Hales T","year":"2017","unstructured":"Hales T, Adams M, Bauer G, et al. A formal proof of the Kepler conjecture[C]\/\/Forum of mathematics, Pi. Cambridge University Press, 2017, 5: e2."},{"key":"e_1_3_3_1_8_2","volume-title":"Generative language modeling for automated theorem proving[J]. arXiv preprint arXiv:2009.03393","author":"Polu S","year":"2020","unstructured":"Polu S, Sutskever I. Generative language modeling for automated theorem proving[J]. arXiv preprint arXiv:2009.03393, 2020."},{"key":"e_1_3_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-021-04086-x"},{"key":"e_1_3_3_1_10_2","volume-title":"Theorem proving with the real numbers[M]","author":"Harrison J.","year":"2012","unstructured":"Harrison J. Theorem proving with the real numbers[M]. Springer Science & Business Media, 2012."},{"key":"e_1_3_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.26969\/d.cnki.gbydu.2022.000016"},{"key":"e_1_3_3_1_12_2","unstructured":"Kelley J L. General Topology [M]. New York: Springer-Verlag 1955."},{"key":"e_1_3_3_1_13_2","volume-title":"Axiomatic Set Theory Machine Proof System (in Chinese) [M]","author":"Yu Wensheng","year":"2020","unstructured":"Yu Wensheng, Sun Tianyu, Fu Yaoshun. Axiomatic Set Theory Machine Proof System (in Chinese) [M]. Beijing: Science Press, 2020."},{"key":"e_1_3_3_1_14_2","volume-title":"Foundations of analysis[M]","author":"Landau E.","year":"2022","unstructured":"Landau E. Foundations of analysis[M]. American Mathematical Society, 2022."},{"key":"e_1_3_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.26969\/d.cnki.gbydu.2024.000519"},{"key":"e_1_3_3_1_16_2","first-page":"6683","article-title":"Formalization of Dedekind Fundamental Theorem in Coq[C]\/\/2023 China Automation Congress (CAC)","volume":"2023","author":"Leng S","unstructured":"Leng S, Guo D, Yu W. Formalization of Dedekind Fundamental Theorem in Coq[C]\/\/2023 China Automation Congress (CAC). IEEE, 2023: 6683-6687.","journal-title":"IEEE"}],"event":{"name":"ICCMS 2025: 2025 The 17th International Conference on Computer Modeling and Simulation (ICCMS)","location":"Zhuhai China","acronym":"ICCMS 2025"},"container-title":["Proceedings of the 2025 17th International Conference on Computer Modeling and Simulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3761668.3761673","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T11:10:14Z","timestamp":1765365014000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3761668.3761673"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,13]]},"references-count":16,"alternative-id":["10.1145\/3761668.3761673","10.1145\/3761668"],"URL":"https:\/\/doi.org\/10.1145\/3761668.3761673","relation":{},"subject":[],"published":{"date-parts":[[2025,6,13]]},"assertion":[{"value":"2025-12-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}