Usable Computer-Checked Proofs and Computations for Number Theorists
Project funded by the Dutch Research Council (NWO) Vidi grant number
016.Vidi.189.037 from January 2019 to December 2023
Principal investigator: Jasmin Blanchette
Host institution: Vrije Universiteit Amsterdam
Summary
Proof assistants (also called interactive theorem provers) are
increasingly used in academia and industry to verify the correctness
of hardware, software, and protocols. However, despite the
trustworthiness guarantees they offer, most mathematicians find them
too laborious to use.
The goal of the Lean Forward project is to collaborate with number
theorists to formally prove theorems about research mathematics and
to address the main usability issues hampering the adoption of proof
assistants in mathematical circles. The theorems will be selected
together with our collaborators to guide the development of formal
libraries and verified tools.
Our vehicle will be Lean, a disruptive proof assistant developed at
Microsoft Research and Carnegie Mellon University. Lean draws on
decades of experience in interactive and automatic theorem provers
(e.g., Coq, Isabelle/HOL, and Z3). Its logic is very expressive, and
emphasis is placed on strong proof automation. The system is easy to
extend via metaprograms that rely on the same logical language that
is used to express specifications and proofs.
To support the formalization of theorems, we will develop formal
libraries of fundamental number theory and explore how to automate
proof search in these. Among many other things, we will create
libraries for p-adic numbers and integers and design reasoning
procedures for these, exploring how to best exploit Lean's
metaprogramming framework. Moreover, we will develop techniques and
tools that help mathematicians perform accurate computations and
reasoning using proof assistants, integrating procedures from
computer algebra systems in a foundational, verified fashion.
Finally, we will contribute to Lean's development with ideas and
features designed to benefit all users, notably an efficient
built-in procedure for first-order reasoning and an integration with
automatic theorem provers. The ultimate aim is to develop a proof
assistant that actually helps mathematicians, by making them more
productive and more confident in their results.
Context
Proof assistants (also called interactive theorem provers) are
interactive tools that make it possible to develop computer-checked,
formal proofs of theorems. Two early systems, Automath and Mizar,
were designed to mechanize mathematics. Landmark achievements
include the formal proofs of the Kepler conjecture by Hales et al.
and of the odd-order theorem by Gonthier et al.
The main strength of proof assistants is their trustworthiness: all
definitions and lemmas are checked for well-formedness, and even the
most trivial proof steps are verified by an inference kernel with
respect to a logical system. It took a formal proof to dispel doubts
about Hales's proof.
Beyond trustworthiness, formal proofs can also clarify arguments, by
exposing and explaining difficult steps. Even without developing any
proofs, making theorem statements (including the definitions and
hypotheses they rely on) precise can be a substantial gain for
communicating results and for making the vast body of mathematics
analyzable by computers.
Moreover, by keeping track of changes across large developments,
proof assistants facilitate experiments with variants and
extensions. When changing a definition, the user is alerted to the
inferences that need repair and to redundant definitions, lemmas,
and hypotheses.
Finally, modern proof assistants provide automatic proof search that
can find long deduction chains quickly, easily beating pen-and-paper
methods. Automation is especially useful for highly computational
proofs with hundreds or thousands of cases. Despite the success
stories, proof assistants can be tedious to use. Most mathematicians
find them more of a hindrance than a help. Today, the main users are
in hardware verification and programming language research.
Despite the many obstacles, there is a strong feeling in various parts
of the research community that mathematics deserves to be formalized.
Fields medalist Vladimir Voevodsky has been one of the strongest
advocates of this view. His research area was plagued by flawed
theorems, to the point where he stopped believing pen-and-paper
arguments.
With the emergence of huge computational proofs, the issue of peer
reviewing is becoming more pressing. There are many disputed theorems,
including Mochizuki's claimed proof of the abc conjecture. It
sometimes happens that articles pass peer review, and get published
in prestigious journals such as the Annals of Mathematics, before it
emerges that a lemma is flawed and the entire proof collapses. More
applied branches of research, such as cryptography, are also subject
to controversies. By relying to a greater extent on computers to
develop and check proofs, researchers can raise the reviewing
standards, even for computational proofs, thereby increasing
confidence in the results' validity.
Challenges
& Objectives
Interactive theorem proving is steadily gaining ground. In some
areas of computer science, it is common for research papers to be
accompanied by formal proofs. Proof assistants are even deployed in
the classroom, replacing pen and paper. These circumstances point to
a future where these tools will be routinely used, resulting in more
reliable science. But to have a substantial impact on mathematical
practice, we must narrow the usability gap.
The difficulties are as much social as technical. Proof assistants
are developed primarily by computer scientists. Much of the
formalized mathematics is motivated by hardware or software
verification. Mathematicians largely dismiss proof assistants as
impractical, so the technology improves only slowly. Sadly, even
routine operations such as factorization of polynomials can become
small challenges when moving to a formal-logic environment. We want
to break the vicious circle by working closely with mathematicians.
We aim to bring a proof assistant, its automation, and its libraries
further, guided by the needs of mathematicians who understand the
value of proof assistants.
Specifically, we will collaborate with Sander Dahmen and his team at
the VU Amsterdam to formalize parts of the team's research in number
theory and recent results in related areas, addressing usability
issues as they arise. Cooperation with research mathematicians will
benefit Lean Forward substantially: not only will they guide us
through their field and help us carry out the formalization, they
will provide frank feedback on our technology and act as advocates
for formal verification in their community.
Our vehicle will be the Lean proof assistant. Lean is a new open
source system developed by Leonardo de Moura (Microsoft Research),
Jeremy Avigad (Carnegie Mellon), and their colleagues. The system's
design and engineering is unusually clean and efficient. Lean
attempts to combine the best from two leading proof assistants:
Lean's logical foundation is a variant of
Coq's calculus of inductive constructions, a dependent type theory.
Lean distinguishes itself with its small inference kernel and strong
automation. Independent proof checkers provide additional
guarantees. Lean's support for dependent types is smoother than
Coq's, thanks to flexible pattern matching and a generalized
congruence closure algorithm. A mechanism for introducing quotient
types and a transfer tool facilitate reasoning up to isomorphism
without resorting to setoids or homotopy type theory.
For the design of basic algebraic
libraries, Lean's developers turned to Isabelle/HOL for inspiration.
The libraries rely on type classes, a mechanism to categorize types
and their operations (e.g., "(Z, +) forms a group"). Type classes
interact well with Lean's dependent types. By contrast, in
Isabelle/HOL, there is no way to use type classes to reason about
the integers modulo n as a ring.
Our overall aim will be met by pursuing four scientific objectives,
presented below. Our starting point is that there is tremendous
value in simultaneously using and developing a proof assistant. Lean
Forward combines these two activities.
OBJECTIVE 1
Formally prove carefully selected theorems about research number theory
From the mathematicians' point of view, formalization can increase
the trustworthiness of their results and the lucidity of their
proofs, while raising awareness of formal verification in the
mathematics community. From a computer science perspective,
formalization will guide the development of proving
technology.
We will formalize theorems emerging from Dahmen's research,
notably in the context of his Vidi project
New Diophantine Directions, as well as other theorems that interest him and his team.
Moreover, we will participate in Hales's
Formal Abstracts
initiative, which aims at enticing mathematicians to state their
theorems formally in Lean, including any definitions they rely on.
Published articles will be complemented by these formal abstracts.
Even such lightweight computerization can be a challenge, which is
indicative of the inherent difficulty of making mathematics
rigorous. Formal abstracts can serve as a gateway to formal proofs
and can be used by powerful automatic search mechanisms.
Russell quipped that "the method of 'postulating' what we want has
many advantages; they are the same as the advantages of theft over
honest toil." However, for most mathematicians, this
fundamentalism is unrealistic. Modern research on
Diophantine equations often depends on the modularity of elliptic
curves, which constitutes the final step in the proof of Fermat's
last theorem and relies on an overwhelming amount of theory. Full
formalization being unrealistic, we will embrace flexible levels
of formality.
OBJECTIVE 2
Develop formal libraries of fundamental number theory and explore how to automate proof search
This objective is linked to the first objective: we will develop
libraries guided by the theorems we aim at formalizing, but we
will also choose the theorems to produce useful reusable libraries
as a side effect. We will also help develop missing basic
libraries, contributing to the
Lean mathlib. The design of formal mathematical libraries poses many
challenges.
- Usable design: The experience with building large formal libraries is that textbook lemmas and theorems do not suffice. A lot of scaffolding—mathematically trivial but practically crucial aspects, such as naming conventions, idioms, and syntax—is necessary for usability.
- Proof readability: Many formal proofs are "write only." In our proofs, the important steps will be clearly identified, using Lean's Mizar-like declarative style. Declarative proofs can be used to communicate with mathematicians and are easier to port across systems.
- Strong automation: A good formal library includes heuristics and algorithms—tactics. Lean's revolutionary metaprogramming framework exposes the system's data structures and procedures within the language of Lean itself. Users can comfortably develop tactics in Lean via a monadic interface. Automation can be developed together with the libraries, rather than as an afterthought.
The libraries will be developed with maintainability in mind. To ensure their longevity, we will initiate a repository of third-party Lean formalizations and tools. Our goal is not only to prove lemmas and theorems but also to verify algorithms and use verified algorithms to check entries in online databases (e.g., LMFDB). Beyond their intrinsic appeal, the algorithms often arise naturally in proofs. Moreover, verified algorithms can be used to prove lemmas using reflection.
OBJECTIVE 3
Design techniques and develop tools that help mathematicians carry out accurate computations and reasoning
Many vital tools are missing. Chief among these is a practical
integration of popular computer algebra systems into Lean. These
systems offer a vast collection of algorithms. The main difficulty
is to obtain and reconstruct certificates produced by the algebra
systems, to validate the results in the proof assistant.
Fortunately, for many algorithms, the answers are their own
certificates. We plan to expand the experimental Lean–Mathematica
bridge to cover more algorithms and algebra systems. Some
algorithms are provided by open-source libraries and could be
included in Lean.
Moreover, we plan to integrate our Nunchaku counterexample
generator and complete the integration of the Polya inequality
prover. We will also exploit this opportunity to investigate how
to extend Nunchaku—which relies on satisfiability modulo theories
(SMT) and model finding—to reason about p-adic numbers and
other mathematical entities.
OBJECTIVE 4
Contribute directly to Lean's development with ideas and features designed to increase user productivity
One of the primary objectives with Lean is to bridge the gap
between automatic and interactive theorem proving. A cornerstone
for this vision is white-box automation: the key techniques
underlying SMT solvers, such as the congruence closure for
reasoning about equality and the quantifier instantiation
heuristics are available to users via the metaprogramming
framework. Despite this, several reasoning components, as well as
some important metaprogramming "tape and glue," are missing.
We will design a cohesive set of reasoning components.
We also want to contribute to the Lean simplifier's support for
arithmetic and the envisioned algebraic normalizer. The main
difficulty is to balance raw deductive power, extensibility, and
predictability. Furthermore, we will design a relevance filter
that selects lemmas from background libraries, for use with
tactics. One of the challenges is to perform the heuristic
selection in a robust way, so that filtering can be used both for
proof search and for rechecking the proof.
Finally, it will be useful to integrate external automatic theorem
provers in Lean. A new generation of higher-order provers is
emerging—including Leo-III, Satallax, and higher-order versions of
CVC4, E, Vampire, veriT, and Zipperposition. The
Matryoshka project
funds work on E and veriT. Integrating these provers will
dramatically increase automation. The challenge is to design a
sound, complete, and yet efficient encoding of Lean's rich type
system, and to reconstruct proofs in Lean.
The Lean Forward Team
Funded by the project
Associated members
Collaborators
Publications
2024
The Hitchhiker's Guide to Logical Verification
Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg.
Book (A4, PDF) ⋅ Book (A5, PDF)2023
Recurrence-driven summations in automated deduction
Visa Nummelin, Jasmin Blanchette, and Sander R. Dahmen. In Sattler, U., Suda, M. 14th International Symposium on Frontiers of Combining Systems (FroCoS 2023), LNCS, Springer, 2023.
Authors' PDF Report (PDF)Finding mathematical proofs using computers
Alexander Bentkamp and Jasmin Blanchette. Nieuw Archief voor Wiskunde 5/24(2): 114–118, 2023.
Publisher's PDF Authors' PDFMechanical mathematicians
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Communications of the ACM 66(4): 80–90, 2023.
Publisher's page Authors' PDFSAT-inspired higher-order eliminations
Jasmin Blanchette and Petar Vukmirović. Logical Methods in Computer Science 19(2), 2023.
Publisher's page Authors' PDFSAT-inspired eliminations for superposition
Petar Vukmirović, Jasmin Blanchette, and Marijn J.H. Heule. Transactions on Computational Logic 24(1): article 7, 2023.
Publisher's page Authors' PDFUnifying splitting
Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret. Journal of Automated Reasoning 67, article number 10, 2023.
Publisher's page Authors' PDF
Aesop: White-box best-first proof search for Lean
Jannis Limperg and Asta Halkjær From. 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), ACM, 2023.
Publisher's page Authors' PDFVerified given clause procedures
Jasmin Blanchette, Qi Qiu, and Sophie Tourret. In Pientka, B., Tinelli, C. 29th International Conference on Automated Deduction (CADE-29), LNCS, Springer, 2023.
Authors' PDF
Closure properties of general grammars–formally verified
Martin Dvorak and Jasmin Blanchette. In Naumowicz, A., Thiemann, R. 14th International Conference on Interactive Theorem Proving (ITP 2023), LIPIcs ???, pages 11:1–11:16, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2023.
Publisher's page Authors' PDF
Premise Selection for Lean 4
Alistair Geesing. MSc thesis, Vrije Universiteit Amsterdam, 2023.
Thesis (PDF)
A Deep Embedding of μCRL in Lean
Wolf bij 't Vuur. MSc thesis, Vrije Universiteit Amsterdam, 2023.
Thesis (PDF)
Implementing a Definitional (Co)datatype Package in Lean 4, Based on Quotients of Polynomial Functors
Alex C. Keizer. MSc thesis, Universiteit van Amsterdam, 2023.
Thesis (PDF)Superposition for higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. Journal of Automated Reasoning 67, article number 10, 2023.
Publisher's page Authors' PDF Errata (PDF)Extending a high-performance prover to higher-order logic
Petar Vukmirović, Jasmin Blanchette, and Stephan Schulz. In 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), LNCS 13994, pp. 111–129, Springer, 2023.
Publisher's page Authors' PDF2022
A bi-directional extensible interface between Lean and Mathematica
Robert Y. Lewis and Minchao Wu. Journal of Automated Reasoning 66(2): 215–238, 2022.
Publisher's page Authors' PDF
A formalization of Dedekind domains and class groups of global fields
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio. Journal of Automated Reasoning 66(4): 611–637, 2022.
Publisher's page
Use and abuse of instance parameters in the Lean mathematical library
Anne Baanen. In Andronick, J., de Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022), LIPIcs 237, pages 4:1–4:20, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2022.
Publisher's pageA comprehensive framework for saturation theorem proving
Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. Journal of Automated Reasoning 66(4): 499–539, 2022.
Publisher's page Authors' PDFMaking higher-order superposition work
Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Journal of Automated Reasoning 66(4): 541–564, 2022.
Publisher's page Authors' PDFExtending a brainiac prover to lambda-free higher-order logic
Petar Vukmirović, Jasmin Blanchette, Simon Cruanes, and Stephan Schulz. International Journal on Software Tools for Technology Transfer 24(1): 67–87, 2022.
Publisher's page Authors' PDFSeventeen provers under the hammer
Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. In Andronick, J., de Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022), LIPIcs 237, pages 8:1–8:18, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2022.
Publisher's page Authors' PDF2021
Efficient full higher-order unification
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Logical Methods in Computer Science 17(4): 18:1–18:31, 2021.
Authors' PDFSuperposition with lambdas
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Journal of Automated Reasoning 65(7): 893–940, 2021.
Publisher's page Authors' PDF
Verifying AVL Trees in Lean
Sofia Konovalova. BSc thesis, Vrije Universiteit Amsterdam, 2021.
Thesis (PDF)
A Graph Library for Lean 4
Peter Kementzey. BSc thesis, Vrije Universiteit Amsterdam, 2021.
Thesis (PDF)Superposition for lambda-free higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann. Logical Methods in Computer Science 17(2): 1:1–1:38, 2021.
Publisher's page Authors' PDFSAT-inspired eliminations for superposition
Petar Vukmirović, Jasmin Blanchette, and Marijn J.H. Heule. In Piskac, R., Whalen, M. (eds.) 21st International Conference on Formal Methods in Computer-Aided Design (FMCAD 2021), pp. 231–240, IEEE, 2021.
Publisher's page Authors' PDF Report (PDF)
Disseminating a Library of Formal Proofs for Flexible and Persistent Searching
Polina Boneva. BSc thesis, Vrije Universiteit Amsterdam, 2021.
Thesis (PDF)
A formalization of Dedekind domains and class groups of global fields
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio. In Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021), LIPIcs 193, pp. 5:1–5:19, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2021.
Publisher's page Authors' PDFSuperposition with first-class Booleans and inprocessing clausification
Visa Nummelin, Alexander Bentkamp, Sophie Tourret, and Petar Vukmirović. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS 12699, pp. 378–395, Springer, 2021.
Publisher's page Authors' PDF Report (PDF) Errata (PDF)A unifying splitting framework
Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS 12699, pp. 344–360, Springer, 2021.
Publisher's page Authors' PDF Report (PDF)Superposition for full higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS 12699, pp. 396–412, Springer, 2021.
Publisher's page Authors' PDF Report (PDF) Errata (PDF)Making higher-order superposition work
Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS 12699, pp. 415–432, Springer, 2021.
Publisher's page Authors' PDF
A novice-friendly induction tactic for Lean
Jannis Limperg. In Hrițcu, C., Popescu, A. (eds.) 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), pp. 199–211, ACM, 2021.
Publisher's page Author's PDF
Formalizing the ring of Witt vectors
Johan Commelin and Robert Y. Lewis. In Hrițcu, C., Popescu, A. (eds.) 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), pp. 264–277, ACM, 2021.
Publisher's page Authors' PDFA modular Isabelle framework for verifying saturation provers
Sophie Tourret and Jasmin Blanchette. In Hrițcu, C., Popescu, A. (eds.) 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), pp. 224–237, ACM, 2021.
Publisher's page Authors' PDF2020
Simplifying casts and coercions
Robert Y. Lewis and Paul-Nicolas Madelaine. Accepted at Seventh Workshop on Practical Aspects of Automated Reasoning (PAAR-2020).
Authors' PDF
Maintaining a library of formal mathematics
Floris van Doorn, Gabriel Ebner, and Robert Y. Lewis. In Benzmüller, C., Miller, B. (eds.) 13th Conference on Intelligent Computer Mathematics (CICM 2020), LNCS 12236, pp. 251 267, Springer, 2020.
Publisher's page Authors' PDF
A Lean tactic for normalising ring expressions with exponents (short paper)
Anne Baanen. In Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Part II, LNCS 12167, pp. 21–27, Springer, 2020.
Publisher's page Authors' PDFA comprehensive framework for saturation theorem proving
Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. In Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Part I, LNCS 12166, pp. 316–334, Springer, 2020.
Publisher's page Authors' PDF Report (PDF)
The Lean mathematical library
The mathlib Community. In Blanchette, J., Hrițcu, C. (eds.) 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381, ACM, 2020.
Publisher's page Authors' PDFFormalizing Bachmair and Ganzinger's ordered resolution prover
Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, and Uwe Waldmann. Journal of Automated Reasoning 64(7): 1169–1195, 2020.
Online viewer Publisher's page Authors' PDF2019
Arithmetic and Casting in Lean
Paul-Nicolas Madelaine. MSc internship report, Vrije Universiteit Amsterdam, 2019.
Report (PDF)
Verification of GPU Program Optimizations in Lean
Björn Fischer. MSc thesis, Vrije Universiteit Amsterdam, 2019.
Thesis (PDF)
Formalizing the solution to the cap set problem
Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. In Harrison, J., O'Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019), LIPIcs 141, pp. 15:1–15:19, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2019.
Publisher's page Authors' PDF Proof sketch (PDF)Superposition with lambdas
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 55–73, Springer, 2019.
Publisher's page Authors' PDF Report (PDF)Extending a brainiac prover to lambda-free higher-order logic
Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, and Stephan Schulz. In Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), LNCS 11427, pp. 192–210, Springer, 2019.
Publisher's page Authors' PDF Report (PDF)
A formal proof of Hensel's lemma over the p-adic integers
Robert Y. Lewis. In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), pp. 15–26, ACM, 2019.
Publisher's page Author's PDF
An Implementation of Buchberger's Algorithm in Lean
Markos Dermitzakis. BSc thesis, Vrije Universiteit Amsterdam, 2019.
Thesis (PDF)Efficient full higher-order unification
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. In Ariola, Z.M. (ed.), 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), LIPIcs 167, pp. 5:1–5:17, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2020.
Publisher's page Authors' PDF Report (PDF)Boolean reasoning in a higher-order superposition prover
Petar Vukmirović and Visa Nummelin. Presented at 7th Workshop on Practical Aspects of Automated Reasoning (PAAR-2020).
Authors' PDF2018
Meta-programming with the Lean Proof Assistant
Pablo Le Hénaff. MSc internship report, École Polytechnique Paris, 2018.
Thesis (PDF)
A Formally Verified Proof of the Mason–Stothers Theorem in Lean
Jens Wagemaker. BSc thesis, Vrije Universiteit Amsterdam, 2018.
Thesis (PDF)Events
Logic and Modelling 2022–2023
Period 5 of 2022–2023, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturer: Anne Baanen.
Logical Verification 2022–2023
Period 2 of 2022–2023, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturers: Jasmin Blanchette and Jannis Limperg.
Logic and Modelling 2021–2022
Period 5 of 2021–2022, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturer: Jasmin Blanchette.
Machine-Checked Mathematics
2–4 March 2022, virtually.
Logical Verification 2021–2022
Period 2 of 2021–2022, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturer: Jasmin Blanchette. Guest lecturer: Alex J. Best
Logic and Modelling 2020–2021
Period 5 of 2020–2021, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturers: Robert Y. Lewis and Jasmin Blanchette.
Lean Together 2021
4–7 January 2021, virtually.
Logical Verification 2020–2021
Period 2 of 2020–2021, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturers: Jasmin Blanchette and Gabriel Ebner. Guest lecturer: Robert Y. Lewis.
Logic and Modelling 2019–2020
Period 5 of 2019–2020, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturer: Robert Y. Lewis.
Logical Verification 2019–2020
Period 2 of 2019–2020, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturers: Alexander Bentkamp and Jasmin Blanchette. Guest lecturers: Anne Baanen and Robert Y. Lewis.
Logic and Modelling 2018–2019
Period 5 of 2018–2019, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturer: Robert Y. Lewis.
Lean Together 2019
7–11 January 2019, Amsterdam, the Netherlands.
Logical Verification 2018–2019
Period 2 of 2018–2019, Vrije Universiteit Amsterdam, Amsterdam, the Netherlands. Lecturers: Jasmin Blanchette and Johannes Hölzl. Guest lecturer: Robert Y. Lewis.
Contact
Please write to
Jasmin Blanchette for
queries related to the project.
The Zulip chat room Lean
is used by the project's members.
Thanks
The project is thankful for the support and advice of the following friends and colleagues: Alessio d'Arielli, Peter Boven, Wan Fokkink, Cristiano Giuffrida, Mojca Lovrenčak, Roy Overbeek, Anja Palatzke, Lawrence Paulson, Thomas Sturm, Rikkert Stuwe, Mark Summerfield, Susanti Tang-Budiwandojo, and Caroline Waij.