---
title: "The Lean mathematical library — paper by Community (2019)"
description: "The paper describes mathlib, a library of formalized mathematics for the Lean 3 proof assistant. 62 references, cited by 88 papers here."
authors: ["The mathlib Community"]
year: 2019
venue: "arXiv:1910.09336"
source: "https://arxiv.org/abs/1910.09336"
doi: "10.1145/3372885.3373824"
arxiv: "1910.09336"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2019](https://md.research.elamur.ai/free/en/papers/2019/page/3/) / The Lean mathematical library

# The Lean mathematical library

**Authors:** The mathlib Community · **Year:** 2019 · **Venue:** arXiv:1910.09336 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://doi.org/10.1145/3372885.3373824) · [PDF](https://arxiv.org/pdf/1910.09336v2) · [DOI 10.1145/3372885.3373824](https://doi.org/10.1145/3372885.3373824) · [arXiv 1910.09336](https://arxiv.org/abs/1910.09336) · [OpenAlex](https://openalex.org/W2981188613)

**Citations:** 161 citations (OpenAlex, 2026-10-14) · [88](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper describes mathlib, a library of formalized mathematics for the Lean 3 proof assistant. A decentralized community builds and maintains it; no single institution runs it. The aim is a single shared base of definitions and proofs that can eventually support research-level mathematics. It also serves as Lean's standard library for programming. The authors explain the foundations: Lean's dependent type theory, based on the calculus of inductive constructions and extended with quotient types and classical axioms. They show how type classes organize a large "structure hierarchy" that links algebraic, order-theoretic and topological notions. They also describe how Lean's metaprogramming framework lets contributors write tactics and automation in Lean itself. Most of the content is still undergraduate level. Even so, it already covers topology, category theory, linear algebra, number theory and very general manifolds. The authors argue that no other proof assistant library combines all of these traits: dependent types, a focus on classical mathematics, built-in automation and a dense network of instances. Contributors include both mathematicians and computer scientists, and this mix shapes where the library goes.

## Key points
- mathlib was split off from Lean's core library in summer 2017. In about two years it grew from 15k to 140k lines of code, not counting blank lines and comments. It has 73 contributors and a team of 11 maintainers.
- On December 12, 2019, the library had 140,085 LOC and 34,168 declarations. The `data` directory was the largest at about 41.8k LOC, followed by `topology` at about 17.4k.
- Notable formalizations:
  - the Gromov–Hausdorff space, proved to be Polish
  - manifolds over any non-discrete normed field (R, C, Q_p)
  - Sylow's theorems, quadratic reciprocity and Hilbert's basis theorem
  - undecidability of the halting problem and Hensel's lemma

  Analysis is still a weaker area.
- The Mathematical Components library relies on canonical structures. mathlib instead uses type class inference, so declaring a single instance (for example, the reals as a metric space) automatically gives the induced structures, such as uniform and topological spaces.
- The paper appeared at CPP '20 under a collective pseudonym. The authors expect to port the library to Lean 4, which will not be backward compatible with Lean 3.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works

## Cite

Cite as: The mathlib Community. 2019. The Lean mathematical library. arXiv:1910.09336.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{community2019lean,
  title = {{The Lean mathematical library}},
  author = {The mathlib Community},
  year = {2019},
  doi = {10.1145/3372885.3373824},
  eprint = {1910.09336},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1145/3372885.3373824}
}
```

- [← previous CLPsych 2019 Shared Task: Predicting the Degree of Suicide Risk in Reddit Posts](https://md.research.elamur.ai/free/en/papers/zirikly-2019-clpsych-2019-shared-task-predicting/)
- [next → Improved Knowledge Distillation via Teacher Assistant](https://md.research.elamur.ai/free/en/papers/mirzadeh-2019-improved-knowledge-distillation-teacher-assistant/)
- [↑ back to papers of 2019](https://md.research.elamur.ai/free/en/papers/2019/page/3/)

## References

62 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. 1994. The QED Manifesto. In Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings. 238–251. [http://link.springer.com/chapter/10.1007/3-540-58156-1_17](http://link.springer.com/chapter/10.1007/3-540-58156-1_17) — [doi:10.1007/3-540-58156-1_17](https://doi.org/10.1007/3-540-58156-1_17) [↗](http://link.springer.com/chapter/10.1007/3-540-58156-1_17)
2. Reynald Affeldt, Cyril Cohen, and Damien Rouhling. 2018. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. J. Formalized Reasoning 11, 1 (2018), 43–76. https://doi.org/10.6092/issn.1972-5787/8124 — [doi:10.6092/issn.1972-5787/8124](https://doi.org/10.6092/issn.1972-5787/8124) [↗](https://doi.org/10.6092/issn.1972-5787/8124)
3. Jesús Aransay and Jose Divasón. 2014. Formalization and Execution of Linear Algebra: From Theorems to Algorithms. In Logic-Based Program Synthesis and Transformation, Gopal Gupta and Ricardo Peña (Eds.). Springer International Publishing, Cham, 1–18. https://doi.org/10.1007/978-3-319-14125-1_1 — [doi:10.1007/978-3-319-14125-1_1](https://doi.org/10.1007/978-3-319-14125-1_1) [↗](https://doi.org/10.1007/978-3-319-14125-1_1)
4. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. 2009. Hints in Unification. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. 84–98. https://doi.org/10.1007/978-3-642-03359-9_8 — [doi:10.1007/978-3-642-03359-9_8](https://doi.org/10.1007/978-3-642-03359-9_8) [↗](https://doi.org/10.1007/978-3-642-03359-9_8)
5. Jeremy Avigad, Leonardo de Moura, and Soonho Kong. 2014. Theorem Proving in Lean. Carnegie Mellon University. [find](https://scholar.google.com/scholar?q=Jeremy+Avigad%2C+Leonardo+de+Moura%2C+and+Soonho+Kong%2E+2014%2E+Theorem+Proving+in+Lean%2E+Carnegie+Mellon+University%2E)
6. Seulkee Baek. 2019. Reflected Decision Procedures in Lean. Master’s thesis. Carnegie Mellon University. [http://www.andrew.cmu.edu/user/avigad/Students/baek_ms_thesis.pdf](http://www.andrew.cmu.edu/user/avigad/Students/baek_ms_thesis.pdf) [↗](http://www.andrew.cmu.edu/user/avigad/Students/baek_ms_thesis.pdf)
7. Clemens Ballarin. 2003. Locales and Locale Expressions in Isabelle/Isar. In Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. 34–50. https://doi.org/10.1007/978-3-540-24849-1_3 — [doi:10.1007/978-3-540-24849-1_3](https://doi.org/10.1007/978-3-540-24849-1_3) [↗](https://doi.org/10.1007/978-3-540-24849-1_3)
8. Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. 2018. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. J. Autom. Reasoning 61, 1-4 (2018), 9–32. https://doi.org/10.1007/s10817-017-9440-6 — [doi:10.1007/s10817-017-9440-6](https://doi.org/10.1007/s10817-017-9440-6) [↗](https://doi.org/10.1007/s10817-017-9440-6)
9. Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Ko-rniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. 2015. Mizar: State-of-the-art and Beyond. In Intelligent Computer Mathematics, Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (Eds… — [doi:10.1007/978-3-319-20615-8_17](https://doi.org/10.1007/978-3-319-20615-8_17) [find](https://scholar.google.com/scholar?q=Grzegorz+Bancerek%2C+Czes%C5%82aw+Byli%C5%84ski%2C+Adam+Grabowski%2C+Artur+Ko%2Drni%C5%82owicz%2C+Roman+Matuszewski%2C+Adam+Naumowicz%2C+Karol+P%C4%85k%2C+and+Josef+Urban%2E+2015%2E+Mizar%3A+State%2Dof%2Dthe%2Dart+and+Beyond%2E+In+Intelligent+Compute)
10. Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Springer. https://doi.org/10.1007/978-3-662-07964-5 — [doi:10.1007/978-3-662-07964-5](https://doi.org/10.1007/978-3-662-07964-5) [↗](https://doi.org/10.1007/978-3-662-07964-5)
11. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. 2013. Extending Sledgehammer with SMT Solvers. J. Autom. Reasoning 51, 1 (2013), 109–128. https://doi.org/10.1007/s10817-013-9278-5 — [doi:10.1007/s10817-013-9278-5](https://doi.org/10.1007/s10817-013-9278-5) [↗](https://doi.org/10.1007/s10817-013-9278-5)
12. Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, and Tobias Nipkow. 2015. Mining the Archive of Formal Proofs. In Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. 3–17. https://doi.org/10.1007/978-3-319-20615-8… — [doi:10.1007/978-3-319-20615-8_1](https://doi.org/10.1007/978-3-319-20615-8_1) [↗](https://doi.org/10.1007/978-3-319-20615-8…)
13. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. 2016. [Hammering towards QED](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/). J. Formalized Reasoning 9, 1 (2016), 101–148. https://doi.org/10.6092/issn.1972-5787/4593 [↗](https://doi.org/10.6092/issn.1972-5787/4593)
14. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. 2015. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science 9, 1 (2015), 41–62. https://doi.org/10.1007/s11786-014-0181-1 — [doi:10.1007/s11786-014-0181-1](https://doi.org/10.1007/s11786-014-0181-1) [↗](https://doi.org/10.1007/s11786-014-0181-1)
15. Kevin Buzzard, Johan Commelin, and Patrick Massot. 2020. Formalising Perfectoid Spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, January 20-21, 2020. [find](https://scholar.google.com/scholar?q=Kevin+Buzzard%2C+Johan+Commelin%2C+and+Patrick+Massot%2E+2020%2E+Formalising+Perfectoid+Spaces%2E+In+Proceedings+of+the+9th+ACM+SIGPLAN+International+Conference+on+Certified+Programs+and+Proofs%2C+CPP+2020%2C+New+O)
16. Mario Carneiro. 2019. Formalizing Computability Theory via Partial Recursive Functions. In 10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O’Leary, and Andrew Tolmach (Eds.), Vol. 141. Schloss Da… — [doi:10.4230/lipics.itp.2019.12](https://doi.org/10.4230/lipics.itp.2019.12) [find](https://scholar.google.com/scholar?q=Mario+Carneiro%2E+2019%2E+Formalizing+Computability+Theory+via+Partial+Recursive+Functions%2E+In+10th+International+Conference+on+Interactive+Theorem+Proving+%28ITP+2019%29+%28Leibniz+International+Proceedings+in)
17. Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing mathematics with the Nuprl proof development system. Prentice Hall. http://d… [find](https://scholar.google.com/scholar?q=Robert+L%2E+Constable%2C+Stuart+F%2E+Allen%2C+Mark+Bromley%2C+Rance+Cleaveland%2C+J%2E+F%2E+Cremer%2C+R%2E+W%2E+Harper%2C+Douglas+J%2E+Howe%2C+Todd+B%2E+Knoblock%2C+N%2E+P%2E+Mendler%2C+Prakash+Panangaden%2C+James+T%2E+Sasaki%2C+and+Scott+F%2E+Sm)
18. Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. 2019. Formalizing the Solution to the Cap Set Problem. In 10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O’Leary, and Andrew Tolmach (Eds.)… — [doi:10.4230/lipics.itp.2019.15](https://doi.org/10.4230/lipics.itp.2019.15) [find](https://scholar.google.com/scholar?q=Sander+R%2E+Dahmen%2C+Johannes+H%C3%B6lzl%2C+and+Robert+Y%2E+Lewis%2E+2019%2E+Formalizing+the+Solution+to+the+Cap+Set+Problem%2E+In+10th+International+Conference+on+Interactive+Theorem+Proving+%28ITP+2019%29+%28Leibniz+Intern)
19. Leonardo de Moura and Nikolaj Bjørner. 2007. Efficient E-Matching for SMT Solvers. In Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. 183–198. https://doi.org/10.1007/978-3-540-73595-3_13 — [doi:10.1007/978-3-540-73595-3_13](https://doi.org/10.1007/978-3-540-73595-3_13) [↗](https://doi.org/10.1007/978-3-540-73595-3_13)
20. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (system description). [https://leanprover.github.io/papers/system.pdf](https://leanprover.github.io/papers/system.pdf) [↗](https://leanprover.github.io/papers/system.pdf)
21. Jose Divasón and Jesús Aransay. 2013. Rank-Nullity Theorem in Linear Algebra. Archive of Formal Proofs (Jan. 2013). [http://isa-afp.org/entries/Rank_Nullity_Theorem.html](http://isa-afp.org/entries/Rank_Nullity_Theorem.html), Formal proof development. [↗](http://isa-afp.org/entries/Rank_Nullity_Theorem.html)
22. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. 2017. A metaprogramming framework for formal verification. PACMPL 1, ICFP (2017), 34:1–34:29. https://doi.org/10.1145/3110278 — [doi:10.1145/3110278](https://doi.org/10.1145/3110278) [↗](https://doi.org/10.1145/3110278)
23. Jordan S. Ellenberg and Dion Gijswijt. 2017. On large subsets of F q n with no three-term arithmetic progression. Ann. of Math. (2) 185, 1 (2017), 339–343. https://doi.org/10.4007/annals.2017.185.1.8 — [doi:10.4007/annals.2017.185.1.8](https://doi.org/10.4007/annals.2017.185.1.8) [↗](https://doi.org/10.4007/annals.2017.185.1.8)
24. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. 2009. Packaging Mathematical Structures. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. 327–342. https://doi.org/10.1007/978-3-642-0335… — [doi:10.1007/978-3-642-03359-9_23](https://doi.org/10.1007/978-3-642-03359-9_23) [↗](https://doi.org/10.1007/978-3-642-0335…)
25. Michèle Giry. 1982. A categorical approach to probability theory. In Categorical aspects of topology and analysis (Ottawa, Ont., 1980). Lecture Notes in Math., Vol. 915. Springer, Berlin-New York, 68–85. https://doi.org/10.1007/BFb0092872 — [doi:10.1007/bfb0092872](https://doi.org/10.1007/bfb0092872) [↗](https://doi.org/10.1007/BFb0092872)
26. Georges Gonthier. 2011. Point-Free, Set-Free Concrete Linear Algebra. In Interactive Theorem Proving, Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 103–118. https://doi.org/10.1007/978-3-642-22863-6_10 — [doi:10.1007/978-3-642-22863-6_10](https://doi.org/10.1007/978-3-642-22863-6_10) [↗](https://doi.org/10.1007/978-3-642-22863-6_10)
27. Georges Gonthier and Assia Mahboubi. 2010. An introduction to small scale reflection in Coq. J. Formalized Reasoning 3, 2 (2010), 95–152. https://doi.org/10.6092/issn.1972-5787/1979 — [doi:10.6092/issn.1972-5787/1979](https://doi.org/10.6092/issn.1972-5787/1979) [↗](https://doi.org/10.6092/issn.1972-5787/1979)
28. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. 2010. Mizar in a Nutshell. Journal of Formalized Reasoning 3, 2 (2010), 153– 245. https://doi.org/10.6092/issn.1972-5787/1980 — [doi:10.6092/issn.1972-5787/1980](https://doi.org/10.6092/issn.1972-5787/1980) [↗](https://doi.org/10.6092/issn.1972-5787/1980)
29. Adam Grabowski, Artur Kornilowicz, and Christoph Schwarzweller. 2016. On algebraic hierarchies in mathematical repository of Mizar. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gdańsk, Poland, September 11-14, 2016. 363–371. [https://doi.o…](https://doi.o…) — [doi:10.15439/2016f520](https://doi.org/10.15439/2016f520) [↗](https://doi.o…)
30. Benjamin Grégoire and Assia Mahboubi. 2005. Proving Equalities in a Commutative Ring Done Right in Coq. In Theorem Proving in Higher Order Logics, Joe Hurd and Tom Melham (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 98–113. https://doi.org/10.1007/11541868_7 — [doi:10.1007/11541868_7](https://doi.org/10.1007/11541868_7) [↗](https://doi.org/10.1007/11541868_7)
31. Florian Haftmann and Makarius Wenzel. 2006. Constructive type classes in Isabelle. In International Workshop on Types for Proofs and Programs. Springer, 160–174. https://doi.org/10.1007/978-3-540-74464-1_11 — [doi:10.1007/978-3-540-74464-1_11](https://doi.org/10.1007/978-3-540-74464-1_11) [↗](https://doi.org/10.1007/978-3-540-74464-1_11)
32. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu,… [find](https://scholar.google.com/scholar?q=Thomas+C%2E+Hales%2C+Mark+Adams%2C+Gertrud+Bauer%2C+Dat+Tat+Dang%2C+John+Harrison%2C+Truong+Le+Hoang%2C+Cezary+Kaliszyk%2C+Victor+Magron%2C+Sean+McLaughlin%2C+Thang+Tat+Nguyen%2C+Truong+Quang+Nguyen%2C+Tobias+Nipkow%2C+Steven+)
33. Jesse Michael Han and Floris van Doorn. 2019. A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. In 10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O’Leary, and Andrew… — [doi:10.4230/lipics.itp.2019.19](https://doi.org/10.4230/lipics.itp.2019.19) [find](https://scholar.google.com/scholar?q=Jesse+Michael+Han+and+Floris+van+Doorn%2E+2019%2E+A+Formalization+of+Forcing+and+the+Unprovability+of+the+Continuum+Hypothesis%2E+In+10th+International+Conference+on+Interactive+Theorem+Proving+%28ITP+2019%29+%28)
34. Jesse Michael Han and Floris van Doorn. 2020. A Formal Proof of the Independence of the Continuum Hypothesis. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, January 20-21, 2020. [find](https://scholar.google.com/scholar?q=Jesse+Michael+Han+and+Floris+van+Doorn%2E+2020%2E+A+Formal+Proof+of+the+Independence+of+the+Continuum+Hypothesis%2E+In+Proceedings+of+the+9th+ACM+SIGPLAN+International+Conference+on+Certified+Programs+and+P)
35. John Harrison. 2009. HOL Light: An Overview. In Theorem Proving in Higher Order Logics, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 60–66. https://doi.org/10.1007/978-3-642-03359-9_4 — [doi:10.1007/978-3-642-03359-9_4](https://doi.org/10.1007/978-3-642-03359-9_4) [↗](https://doi.org/10.1007/978-3-642-03359-9_4)
36. John Harrison. 2013. The HOL Light Theory of Euclidean Space. J. Autom. Reasoning 50, 2 (2013), 173–190. https://doi.org/10.1007/s10817-012-9250-9 — [doi:10.1007/s10817-012-9250-9](https://doi.org/10.1007/s10817-012-9250-9) [↗](https://doi.org/10.1007/s10817-012-9250-9)
37. Hao Huang. 2019. Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture. arXiv preprint arXiv:1907.00847 (2019). — [arXiv:1907.00847](https://arxiv.org/abs/1907.00847) [find](https://scholar.google.com/scholar?q=Hao+Huang%2E+2019%2E+Induced+subgraphs+of+hypercubes+and+a+proof+of+the+Sensitivity+Conjecture%2E+arXiv+preprint+arXiv%3A1907%2E00847+%282019%29%2E+%E2%80%94+%5BarXiv%3A1907%2E00847%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1907%2E00847%29)
38. Fabian Immler and Bohua Zhan. 2019. Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. 65–77. https://doi.org/10.1145/3293880.329409… — [doi:10.1145/3293880.3294093](https://doi.org/10.1145/3293880.3294093) [↗](https://doi.org/10.1145/3293880.329409…)
39. C. Kaliszyk and K. Pąk. 2017. Progress in the independent certification of mizar mathematical library in isabelle. In 2017 Federated Conference on Computer Science and Information Systems (FedCSIS). 227–236. https://doi.org/10.15439/2017F289 — [doi:10.15439/2017f289](https://doi.org/10.15439/2017f289) [↗](https://doi.org/10.15439/2017F289)
40. Cezary Kaliszyk, Karol Pąk, and Josef Urban. 2016. Towards a Mizar Environment for Isabelle: Foundations and Language. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016). ACM, New York, NY, USA, 58–65. https://doi.org/10.1145/2854065.2854070 — [doi:10.1145/2854065.2854070](https://doi.org/10.1145/2854065.2854070) [↗](https://doi.org/10.1145/2854065.2854070)
41. Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. 1999. Locales - A Sectioning Concept for Isabelle. In Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Nice, France, September, 1999, Proceedings. 149–166. https://doi.org/10.1007/3-540-48256-3_11 — [doi:10.1007/3-540-48256-3_11](https://doi.org/10.1007/3-540-48256-3_11) [↗](https://doi.org/10.1007/3-540-48256-3_11)
42. M. Kaufmann, P. Manolios, and J.S. Moore. 2000. Computer-Aided Reasoning: ACL2 Case Studies. Advances in Formal Methods, Vol. 4. Springer US. https://doi.org/10.1007/978-1-4757-3188-0 — [doi:10.1007/978-1-4757-3188-0](https://doi.org/10.1007/978-1-4757-3188-0) [↗](https://doi.org/10.1007/978-1-4757-3188-0)
43. Holden Lee. 2014. Vector Spaces. Archive of Formal Proofs (2014). [http://isa-afp.org/entries/VectorSpace.html](http://isa-afp.org/entries/VectorSpace.html), Formal proof development. [↗](http://isa-afp.org/entries/VectorSpace.html)
44. Robert Y. Lewis. 2019. A formal proof of Hensel’s lemma over the p-adic integers. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. 15–26. https://doi.org/10.1145/3293880.3294089 — [doi:10.1145/3293880.3294089](https://doi.org/10.1145/3293880.3294089) [↗](https://doi.org/10.1145/3293880.3294089)
45. Paul-Nicolas Madelaine. 2019. Arithmetic and casting in Lean. Technical Report. Vrije Universiteit Amsterdam. [https://lean-forward.github.io/internships/arithmetic_and_casting_in_lean.pdf](https://lean-forward.github.io/internships/arithmetic_and_casting_in_lean.pdf) [↗](https://lean-forward.github.io/internships/arithmetic_and_casting_in_lean.pdf)
46. Assia Mahboubi and Enrico Tassi. 2017. Mathematical Components. [https://math-comp.github.io/mcb/](https://math-comp.github.io/mcb/) [↗](https://math-comp.github.io/mcb/)
47. Norman Megill and David A. Wheeler. 2019. Metamath: A Computer Language for Mathematical Proofs. Lulu Press. [find](https://scholar.google.com/scholar?q=Norman+Megill+and+David+A%2E+Wheeler%2E+2019%2E+Metamath%3A+A+Computer+Language+for+Mathematical+Proofs%2E+Lulu+Press%2E)
48. Walther Neuper. 2019. Technologies for "Complete, Transparent & Interactive Models of Math" in Education. Electronic Proceedings in Theoretical Computer Science 290 (03 2019), 76–95. https://doi.org/10.4204/EPTCS.290.6 — [doi:10.4204/eptcs.290.6](https://doi.org/10.4204/eptcs.290.6) [↗](https://doi.org/10.4204/EPTCS.290.6)
49. Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science & Business Media. https://doi.org/10.1007/3-540-45949-9 — [doi:10.1007/3-540-45949-9](https://doi.org/10.1007/3-540-45949-9) [↗](https://doi.org/10.1007/3-540-45949-9)
50. Sam Owre, John M. Rushby, and Natarajan Shankar. 1992. PVS: A Prototype Verification System. In Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings. 748–752. https://doi.org/10.1007/3-540-55602-8_217 — [doi:10.1007/3-540-55602-8_217](https://doi.org/10.1007/3-540-55602-8_217) [↗](https://doi.org/10.1007/3-540-55602-8_217)
51. Karol Pak. 2016. Topological Foundations for a Formal Theory of Manifolds. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathe… [find](https://scholar.google.com/scholar?q=Karol+Pak%2E+2016%2E+Topological+Foundations+for+a+Formal+Theory+of+Manifolds%2E+In+Joint+Proceedings+of+the+FM4M%2C+MathUI%2C+and+ThEdu+Workshops%2C+Doctoral+Program%2C+and+Work+in+Progress+at+the+Conference+on+In)
52. Frank Pfenning and Christine Paulin-Mohring. 1989. Inductively Defined Types in the Calculus of Constructions. In Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29 - April 1, 1989, Proceedings. 209–228. https://d… — [doi:10.1007/bfb0040259](https://doi.org/10.1007/bfb0040259) [find](https://scholar.google.com/scholar?q=Frank+Pfenning+and+Christine+Paulin%2DMohring%2E+1989%2E+Inductively+Defined+Types+in+the+Calculus+of+Constructions%2E+In+Mathematical+Foundations+of+Programming+Semantics%2C+5th+International+Conference%2C+Tulan)
53. William Pugh. 1991. The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. In Proceedings of the 1991 ACM/IEEE Conference on Supercomputing (Supercomputing ’91). ACM, New York, NY, USA, 4–13. https://doi.org/10.1145/125826.125848 [↗](https://doi.org/10.1145/125826.125848)
54. Daniel Selsam and Leonardo Moura. 2016. Congruence Closure in Intensional Type Theory. In Proceedings of the 8th International Joint Conference on Automated Reasoning - Volume 9706. Springer-Verlag, Berlin, Heidelberg, 99–115. https://doi.org/10.1007/978-3-319-40229-1_8 — [doi:10.1007/978-3-319-40229-1_8](https://doi.org/10.1007/978-3-319-40229-1_8) [↗](https://doi.org/10.1007/978-3-319-40229-1_8)
55. Konrad Slind and Michael Norrish. 2008. A Brief Overview of HOL4. In Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 28–32. https://doi.org/10.1007/978-3-540-71067-7_6 — [doi:10.1007/978-3-540-71067-7_6](https://doi.org/10.1007/978-3-540-71067-7_6) [↗](https://doi.org/10.1007/978-3-540-71067-7_6)
56. Bas Spitters and Eelis van der Weegen. 2011. Type classes for mathematics in type theory. Mathematical Structures in Computer Science 21, 4 (2011), 795–825. https://doi.org/10.1017/S0960129511000119 — [doi:10.1017/s0960129511000119](https://doi.org/10.1017/s0960129511000119) [↗](https://doi.org/10.1017/S0960129511000119)
57. Sebastian Ullrich and Leonardo de Moura. 2019. Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. arXiv:cs.PL/1908.05647 [find](https://scholar.google.com/scholar?q=Sebastian+Ullrich+and+Leonardo+de+Moura%2E+2019%2E+Counting+Immutable+Beans%3A+Reference+Counting+Optimized+for+Purely+Functional+Programming%2E+arXiv%3Acs%2EPL%2F1908%2E05647)
58. Josef Urban and Geoff Sutcliffe. 2008. ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments. Mathematics in Computer Science 2, 2 (2008), 231–251. https://doi.org/10.1007/s11786-008-0053-7 — [doi:10.1007/s11786-008-0053-7](https://doi.org/10.1007/s11786-008-0053-7) [↗](https://doi.org/10.1007/s11786-008-0053-7)
59. Philip Wadler and Stephen Blott. 1989. How to Make ad-hoc Polymorphism Less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989. 60–76. https://doi.org/10.1145/75277.75283 — [doi:10.1145/75277.75283](https://doi.org/10.1145/75277.75283) [↗](https://doi.org/10.1145/75277.75283)
60. Markus Wenzel. 1997. Type Classes and Overloading in Higher-Order Logic. In Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs’97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings. 307–322. https://doi.org/10.1007/BFb0028402 — [doi:10.1007/bfb0028402](https://doi.org/10.1007/bfb0028402) [↗](https://doi.org/10.1007/BFb0028402)
61. H. P. Williams. 1986. Fourier’s Method of Linear Programming and Its Dual. The American Mathematical Monthly 93, 9 (1986), 681–695. [http://www.jstor.org/stable/2322281](http://www.jstor.org/stable/2322281) [↗](http://www.jstor.org/stable/2322281)
62. Minchao Wu and Rajeev Goré. 2019. Verified Decision Procedures for Modal Logics. In 10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O’Leary, and Andrew Tolmach (Eds.), Vol. 141. Schloss Dagstuhl–… — [doi:10.4230/lipics.itp.2019.31](https://doi.org/10.4230/lipics.itp.2019.31) [find](https://scholar.google.com/scholar?q=Minchao+Wu+and+Rajeev+Gor%C3%A9%2E+2019%2E+Verified+Decision+Procedures+for+Modal+Logics%2E+In+10th+International+Conference+on+Interactive+Theorem+Proving+%28ITP+2019%29+%28Leibniz+International+Proceedings+in+Inform)

*Updated 2 November 2026*