Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover

详细信息    查看全文

• 关键词：Formalization of mathematics ; Algebraic topology
• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9725
• 期：1
• 页码：28-33
• 全文大小：281 KB
• 参考文献：1.Brown, R., Higgins, P.J., Sivera, R.: Nonabelian algebraic topology: filtered spaces, crossed complexes, cubical homotopy groupoids. European Mathematical Society (2011)
  2.de Moura, L., Kong, S., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 378–388. Springer International Publishing, Switzerland (2015)CrossRef
  
• 作者单位：Jakob von Raumer (17)
  
  17. University of Nottingham, Nottingham, UK
  
• 丛书名：Mathematical Software ¨C ICMS 2016
• ISBN：978-3-319-42432-3
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9725

文摘

Lean is a new open source dependently typed theorem prover which is mainly being developed by Leonardo de Moura at Microsoft Research. It is suited to be used for proof irrelevant reasoning as well as for proof relevant formalizations of mathematics. In my talk, I will present my experiences doing a formalization project in Lean. One of the interesting aspects of homotopy type theory is the ability to perform synthetic homotopy theory on higher types. While for the first homotopy group the choice of a suitable algebraic structure to capture the homotopic information is obvious – it’s a group –, implementing a structure to capture the information about both the first and the second homotopy group (or groupoid) of a type and their interactions is more involved. Following Ronald Brown’s book on Nonabelian Algebraic Topology, I formalized two structures: Double groupoids with thin structures and crossed modules on groupoids. I furthermore attempted to prove their equivalence. The project can be seen as a usability and performance test for the new theorem prover.