Fetching the paper…
Reading the bibliography…
This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant.
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Sebastian Ullrich and Leonardo de Moura. 2019 · 1908
Earlier work this paper cites.
Formalization Techniques for Asymptotic Reasoning in Classical Analysis
Reynald Affeldt, Cyril Cohen, and Damien Rouhling. 2018 · 1972
Earlier work this paper cites.
Hammering towards QED
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. 2016 · 1972
Earlier work this paper cites.
An introduction to small scale reflection in Coq
Georges Gonthier and Assia Mahboubi. 2010 · 1979
Earlier work this paper cites.
A categorical approach to probability theory
Michèle Giry. 1982 · 1980
Earlier work this paper cites.
Mizar in a Nutshell
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. 2010 · 1980
Earlier work this paper cites.
Implementing mathematics with the Nuprl proof development system
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 · 1986
Earlier work this paper cites.
Fourier’s Method of Linear Programming and Its Dual
H. P. Williams. 1986 · 1986
Earlier work this paper cites.
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
Frank Pfenning and Christine Paulin-Mohring. 1989 · 1989
Earlier work this paper cites.
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
Philip Wadler and Stephen Blott. 1989 · 1989
Earlier work this paper cites.
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
William Pugh. 1991 · 1991
Earlier work this paper cites.
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
Sam Owre, John M. Rushby, and Natarajan Shankar. 1992 · 1992
Earlier work this paper cites.
The QED Manifesto. In Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings . 238–251
1994 · 1994
Earlier work this paper cites.
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
Markus Wenzel. 1997 · 1997
Earlier work this paper cites.
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
Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. 1999 · 1999
Earlier work this paper cites.
Computer-Aided Reasoning: ACL2 Case Studies . Advances in Formal Methods, Vol. 4
M. Kaufmann, P. Manolios, and J.S. Moore. 2000 · 2000
Earlier work this paper cites.
Isabelle/HOL: a proof assistant for higher-order logic . Vol. 2283
Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002 · 2002
Earlier work this paper cites.
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
Clemens Ballarin. 2003 · 2003
Earlier work this paper cites.
Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions
Yves Bertot and Pierre Castéran. 2004 · 2004
Earlier work this paper cites.
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
Benjamin Grégoire and Assia Mahboubi. 2005 · 2005
Earlier work this paper cites.
Constructive type classes in Isabelle. In International Workshop on Types for Proofs and Programs . Springer, 160–174
Florian Haftmann and Makarius Wenzel. 2006 · 2006
Earlier work this paper cites.
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
Leonardo de Moura and Nikolaj Bjørner. 2007 · 2007
Cited alongside, same era.
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
Konrad Slind and Michael Norrish. 2008 · 2008
Cited alongside, same era.
ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments
Josef Urban and Geoff Sutcliffe. 2008 · 2008
Cited alongside, same era.
Hints in Unification. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings . 84–98
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. 2009 · 2009
Cited alongside, same era.
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
Daniel Selsam and Leonardo Moura. 2016 · 2016
Later among the works it cites.
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. 2017 · 2017
Later among the works it cites.
On large subsets of 𝔽 q n \mathbb{F}^{n}_{q} with no three-term arithmetic progression
Jordan S. Ellenberg and Dion Gijswijt. 2017 · 2017
Later among the works it cites.
A Formal Proof of the Kepler Conjecture
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, Josef Urban, Ky Khac Vu, and Roland Zumkeller. 2017 · 2017
Later among the works it cites.
Progress in the independent certification of mizar mathematical library in isabelle. In 2017 Federated Conference on Computer Science and Information Systems (FedCSIS) . 227–236
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Packaging Mathematical Structures. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings . 327–342
François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. 2009 · 2009
Cited alongside, same era.
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
John Harrison. 2009 · 2009
Cited alongside, same era.
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
Georges Gonthier. 2011 · 2011
Cited alongside, same era.
Type classes for mathematics in type theory
Bas Spitters and Eelis van der Weegen. 2011 · 2011
Cited alongside, same era.
Extending Sledgehammer with SMT Solvers
Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. 2013 · 2013
Cited alongside, same era.
Rank-Nullity Theorem in Linear Algebra
Jose Divasón and Jesús Aransay. 2013 · 2013
Cited alongside, same era.
The HOL Light Theory of Euclidean Space
John Harrison. 2013 · 2013
Cited alongside, same era.
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
Jesús Aransay and Jose Divasón. 2014 · 2014
Cited alongside, same era.
C. Kaliszyk and K. Pąk. 2017 · 2017
Later among the works it cites.
Mathematical Components
Assia Mahboubi and Enrico Tassi. 2017 · 2017
Later among the works it cites.
The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. 2018 · 2018
Later among the works it cites.
Reflected Decision Procedures in Lean
Seulkee Baek. 2019 · 2019
Closest in time.
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 Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 12:1–12:17
Mario Carneiro. 2019 · 2019
Closest in time.
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.), Vol. 141. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 15:1–15:19
Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. 2019 · 2019
Closest in time.
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 Tolmach (Eds.), Vol. 141. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 19:1–19:19
Jesse Michael Han and Floris van Doorn. 2019 · 2019
Closest in time.
Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture
Hao Huang. 2019 · 2019
Closest in time.
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
Fabian Immler and Bohua Zhan. 2019 · 2019
Closest in time.
A formal proof of Hensel’s lemma over the p 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
Robert Y. Lewis. 2019 · 2019
Closest in time.
Arithmetic and casting in Lean
Paul-Nicolas Madelaine. 2019 · 2019
Closest in time.
Metamath: A Computer Language for Mathematical Proofs
Norman Megill and David A. Wheeler. 2019 · 2019
Closest in time.
Technologies for "Complete, Transparent & Interactive Models of Math" in Education
Walther Neuper. 2019 · 2019
Closest in time.
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–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 31:1–31:19
Minchao Wu and Rajeev Goré. 2019 · 2019
Closest in time.
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
Kevin Buzzard, Johan Commelin, and Patrick Massot. 2020 · 2020
Closest in time.
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
Jesse Michael Han and Floris van Doorn. 2020 · 2020
Closest in time.