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.

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. Indeed, it took a formal proof to dispel doubts about Hales's proof of the Kepler conjecture.

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.

There are many obstacles preventing the wide adoption of proof assistants in mathematics.
A zoo of systems
There are many actively developed proof assistants, with incompatible logics and libraries. For example, Coq is based on an expressive logic with dependent types (which facilitate the encoding of abstract algebraic structures), and extensive algebra libraries have been developed for it, but it offers relatively weak proof automation; Isabelle/HOL and HOL Light feature stronger automation and comprehensive analysis libraries but a weaker logic without dependent types; the set-theoretic Mizar system is oriented towards mathematics, but it offers little automation or programmability.
Incomplete mathematical libraries
Formal libraries—consisting of definitions, lemmas, and proofs—are a prerequisite for most formal developments. Before users can apply proof assistants to their own research, they need to formalize a lot of undergraduate and graduate-level mathematics. Even the largest formal libraries cover only a tiny fraction of mathematics.
Weak automation of mathematics
Proof assistants typically combine general-purpose logical automation and procedures for arithmetic. But without domain-specific automation, a single sentence in an informal proof can correspond to dozens or hundreds of lines of formal proof.
Poor interoperability with computer algebra systems
Notwithstanding the existence of a few prototypes, interoperability between computer algebra systems and proof assistants is an open problem. A trustworthy integration of algebra systems in proof assistants requires the validation of certificates produced by the algebra systems. However, most procedures do not generate certificates; for some algorithms, it is not even clear what certificates would look like. Conversely, users of algebra systems could exploit the proof assistants' support for expressing and finding proofs.
Difficult extensibility
Extending proof assistants with procedures for domain-specific reasoning requires a high level of expertise. The programmatic interfaces of the main proof assistants have evolved over several decades and are difficult to learn. For example, to extend Coq, one must typically master both the Ltac tactic language and the low-level OCaml interfaces, in addition to the Gallina specification language.

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.

Proof assistants are powerful, trustworthy tools. If we computer scientists care to listen to interested mathematicians and cooperate with them, we can learn how to direct our tools towards their goals.

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.

Our overall aim is to make proof assistants usable by mathematicians, by initially focusing on number theory and related areas, developing the proof automation, tool integrations, and formal libraries guided by actual users' needs.

The Lean Forward Team

Funded by the project

Jasmin
Blanchette

VU Amsterdam
principal investigator
Jan. 2019 to Dec. 2023

Gabriel
Ebner

VU Amsterdam
postdoc
July 2020 to Sept. 2021

Petar
Vukmirović

VU Amsterdam
PhD student
Feb. 2022 to May. 2022

Anne
Baanen

VU Amsterdam
PhD student
Sept. 2019 to Dec. 2023

Jannis
Limperg

VU Amsterdam
PhD student
Jan. 2020 to Mar. 2023

Visa
Nummelin

VU Amsterdam
PhD student
Mar. 2019 to Dec. 2023

Kevin
Kappelmann

VU Amsterdam
student assistant
April to Sept. 2019

Associated members

Sander
Dahmen

VU Amsterdam

Robert Y.
Lewis

Brown U.

Assia
Mahboubi

Inria Rennes – Bretagne Atlantique &
VU Amsterdam

Aurélien
Saue

VU Amsterdam
intern
March 2021 to August 2021

Freek
Wiedijk

RU Nijmegen

Collaborators

Jeremy
Avigad

Carnegie Mellon U.

Alexander
Bentkamp

HHU Düsseldorf

Leonardo
de Moura

Amazon Web Systems

Femke
van Raamsdonk

VU Amsterdam

Joey
van Langen

VU Amsterdam

Pablo
Le Hénaff

École Polytechnique Paris

Phillip
Lippe

U. Amsterdam

Casper
Putz

VU Amsterdam

Jens
Wagemaker

VU Amsterdam

Publications

= main project-related 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' PDF

Mechanical 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' PDF

SAT-inspired higher-order eliminations

Jasmin Blanchette and Petar Vukmirović. Logical Methods in Computer Science 19(2), 2023.

Publisher's page   Authors' PDF

SAT-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' PDF

Unifying 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' PDF

Verified 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' PDF

2022

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 page

A 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' PDF

Making 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' PDF

Extending 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' PDF

Seventeen 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' PDF

2021

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' PDF

Superposition 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)

Simplicial Sets in Lean

Floris Cnossen. BSc thesis, Universiteit van 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' PDF

SAT-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' PDF

Superposition 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' PDF

A 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' PDF

2020

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' PDF

A 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' PDF

Formalizing 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' PDF

2019

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' PDF

2018

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.