大规模验证

1. ITP

   A Machine-Checked Proof of the Odd Order Theorem Gonthier, Georges, Asperti, Andrea, Avigad, Jeremy, Bertot, Yves, Cohen, Cyril, Garillot, François, Roux, Stéphane Le, Mahboubi, Assia, O’Connor, Russell, Biha, Sidi Ould, Pasca, Ioana, Rideau, Laurence, Solovyev, Alexey, Tassi, Enrico, and Théry, Laurent In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings 2013
2. Forum of Mathematics

   A formal proof of the Kepler conjecture Hales, Thomas C., Adams, Mark, Bauer, Gertrud, Dang, Dat Tat, Harrison, John, Hoang, Truong Le, Kaliszyk, Cezary, Magron, Victor, McLaughlin, Sean, Nguyen, Thang Tat, Nguyen, Truong Quang, Nipkow, Tobias, Obua, Steven, Pleso, Joseph, Rute, Jason M., Solovyev, Alexey, Ta, An Hoai Thi, Tran, Trung Nam, Trieu, Diep Thi, Urban, Josef, Vu, Ky Khac, and Zumkeller, Roland CoRR 2015
3. ASCM

   The Four Colour Theorem: Engineering of a Formal Proof Gonthier, Georges In Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers 2007

验证框架

1. ITP

   Canonical Structures for the Working Coq User Mahboubi, Assia, and Tassi, Enrico In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings 2013

数学分析

1. ITP

   Type Classes and Filters for Mathematical Analysis in Isabelle/HOL Hölzl, Johannes, Immler, Fabian, and Huffman, Brian In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings 2013
2. ITP

   A Formal Proof of Cauchy’s Residue Theorem Li, Wenda, and Paulson, Lawrence C. In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings 2016
3. JAR

   A Verified ODE Solver and the Lorenz Attractor Immler, Fabian J. Autom. Reason. 2018
4. ITP,JAR

   The Flow of ODEs: Formalization of Variational Equation and Poincaré Map Immler, Fabian, and Traut, Christoph J. Autom. Reason. 2019
5. ITP,JAR

   An Isabelle/HOL Formalisation of Green’s Theorem Abdulaziz, Mohammad, and Paulson, Lawrence C. In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings 2016
6. ISSAC

   Verified Real Asymptotics in Isabelle/HOL Eberl, Manuel In Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, ISSAC 2019, Beijing, China, July 15-18, 2019 2019
7. ITP

   A Computer-Algebra-Based Formal Proof of the Irrationality of \(ζ\)(3) Chyzak, Frédéric, Mahboubi, Assia, Sibut-Pinote, Thomas, and Tassi, Enrico In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings 2014
8. ITP

   Formally Verified Approximations of Definite Integrals Mahboubi, Assia, Melquiond, Guillaume, and Sibut-Pinote, Thomas In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings 2016
9. CPP

   Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem Li, Wenda, and Paulson, Lawrence C. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019 2019

代数

1. CPP

   A modular, efficient formalisation of real algebraic numbers Li, Wenda, and Paulson, Lawrence C. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016 2016
2. CPP

   Formalizing jordan normal forms in Isabelle/HOL Thiemann, René, and Yamada, Akihisa In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016 2016
3. CICM

   Gröbner Bases of Modules and Faugère’s F\(_\mbox4\)Algorithm in Isabelle/HOL Maletzky, Alexander, and Immler, Fabian In Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 2018
4. IJCAR

   Algebraically Closed Fields in Isabelle/HOL Vilhena, Paulo Emı́lio, and Paulson, Lawrence C. In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II 2020
5. JAR

   A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm Divasón, Jose, Joosten, Sebastiaan J. C., Thiemann, René, and Yamada, Akihisa J. Autom. Reason. 2020
6. JAR

   Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL Thiemann, René, Bottesch, Ralph, Divasón, Jose, Haslbeck, Max W., Joosten, Sebastiaan J. C., and Yamada, Akihisa J. Autom. Reason. 2020

概率论

1. ITP

   Three Chapters of Measure Theory in Isabelle/HOL Hölzl, Johannes, and Heller, Armin In Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings 2011
2. JAR

   A Formally Verified Proof of the Central Limit Theorem Avigad, Jeremy, Hölzl, Johannes, and Serafin, Luke J. Autom. Reason. 2017
3. CPP

   Markov Chains and Markov Decision Processes in Isabelle/HOL Hölzl, Johannes J. Autom. Reason. 2017

集合论和数理逻辑

1. JAR

   Set Theory for Verification: I. From Foundations to Functions Paulson, Lawrence C. J. Autom. Reason. 1993
2. JAR

   Set Theory for Verification. II: Induction and Recursion Paulson, Lawrence C. J. Autom. Reason. 1995
3. JAR

   Mechanizing Set Theory Paulson, Lawrence C., and Grabczewski, Krzysztof J. Autom. Reason. 1996
4. JAR

   A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle Paulson, Lawrence C. J. Autom. Reason. 2015
5. ITP,JAR

   Formalization of the Fundamental Group in Untyped Set Theory Using Auto2 Zhan, Bohua In Interactive Theorem Proving - 8th International Conference, ITP 2017, Brası́lia, Brazil, September 26-29, 2017, Proceedings 2017
6. ITP

   A Formalization of Forcing and the Unprovability of the Continuum Hypothesis Han, Jesse Michael, and Doorn, Floris In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA 2019
7. IJCAR

   Formalization of Forcing in Isabelle/ZF Gunther, Emmanuel, Pagano, Miguel, and Terraf, Pedro Sánchez In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II 2020

其他高等数学

1. ITP

   Nine Chapters of Analytic Number Theory in Isabelle/HOL Eberl, Manuel In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA 2019
2. CPP

   Smooth manifolds and types to sets for linear algebra in Isabelle/HOL Immler, Fabian, and Zhan, Bohua In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019 2019
3. CPP

   The Poincaré-Bendixson theorem in Isabelle/HOL Immler, Fabian, and Tan, Yong Kiam In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020 2020
4. IJCAR

   Formal Proof of the Group Law for Edwards Elliptic Curves Hales, Thomas C., and Raya, Rodrigo In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II 2020

应用数学

1. Formal Aspects of Computing

   Formal analysis of the kinematic Jacobian in screw theory Shi, Zhiping, Wu, Aixuan, Yang, Xiumei, Guan, Yong, Li, Yongdong, and Song, Xiaoyu Formal Aspects Comput. 2018
2. Formal Aspects of Computing

   Formalization of Camera Pose Estimation Algorithm based on Rodrigues Formula Chen, Shanyan, Wang, Guohui, Li, Ximeng, Zhang, Qianying, Shi, Zhi-Ping, and Guan, Yong Formal Aspects Comput. 2020
3. JAR

   Formalization of Geometric Algebra in HOL Light Li, Li-Ming, Shi, Zhi-Ping, Guan, Yong, Zhang, Qian-Ying, and Li, Yong-Dong J. Autom. Reason. 2019
4. JAR

   Formalization of Euler-Lagrange Equation Set Based on Variational Calculus in HOL Light Guan, Yong, Zhang, Jingzhi, Wang, Guohui, Li, Ximeng, Shi, Zhiping, and Li, Yongdong J. Autom. Reason. 2021