Abstract
We present a new framework for formalizing mathematics in untyped set theory using auto2. Using this framework, we formalize in Isabelle/FOL the entire chain of development from the axioms of set theory to the definition of the fundamental group for an arbitrary topological space. The auto2 prover is used as the sole automation tool, and enables succinct proof scripts throughout the project.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Code available at https://github.com/bzhan/auto2.
- 2.
References
Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reason. 9(1), 101–148 (2016)
Bourbaki, N.: Theory of Sets. Springer, Heidelberg (2000)
Brunerie, G.: On the homotopy groups of spheres in homotopy type theory. Ph.D. thesis. https://arxiv.org/abs/1606.05916
Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. Spec. Issue: User Tutor. I 3(2), 153–245 (2010)
IsarMathLib. http://www.nongnu.org/isarmathlib/
Kaliszyk, C., Pak, K., Urban, J.: Towards a Mizar environment for Isabelle: foundations and language. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016), New York, pp. 58–65 (2016)
Kornilowicz, A., Shidama, Y., Grabowski, A.: The fundamental group. Formalized Math. 12(3), 261–268 (2004)
Kuncar, O.: Reconstruction of the Mizar type system in the HOL light system. In: Pavlu, J., Safrankova, J. (eds.) WDS Proceedings of Contributed Papers: Part I - Mathematics and Computer Sciences, pp. 7–12. Matfyzpress (2010)
Lee, G., Rudnici, P.: Alternative aggregates in Mizar. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM 2007. LNCS (LNAI), vol. 4573, pp. 327–341. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73086-6_26
Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 19–34. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_5
Megill, N.D.: Metamath: a computer language for pure mathematics. http://us.metamath.org/downloads/metamath.pdf
Munkres, J.R.: Topology. Prentice Hall, Upper Saddle River (2000)
Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Automated Reason. 11(3), 353–389 (1993)
Paulson, L.C.: Set theory for verification: II. Induction and recursion. J. Automated Reason. 15(2), 167–215 (1995)
Trybulec, A.: Some features of the Mizar language. In: ESPRIT Workshop (1993)
Wiedijk, F.: Mizar’s soft type system. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 383–399. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74591-4_28
Zhan, B.: AUTO2, a saturation-based heuristic prover for higher-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 441–456. Springer, Cham (2016). doi:10.1007/978-3-319-43144-4_27
Acknowledgements
The author would like to thank the anonymous referees for their comments. This research is completed while the author is supported by NSF Award No. 1400713.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Zhan, B. (2017). Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_32
Download citation
DOI: https://doi.org/10.1007/978-3-319-66107-0_32
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66106-3
Online ISBN: 978-3-319-66107-0
eBook Packages: Computer ScienceComputer Science (R0)