Computations for Number Theorists

Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO) Talent Scheme Vidi 2017 (accepted, yet to be formally activated)
| |

File No. 016.Vidi.189.037 | |

January 2019 – December 2023 (expected)
| |

Principal investigator:
| Jasmin Christian Blanchette, Vrije Universiteit Amsterdam |

Senior collaborators:
| Sander Dahmen, Vrije Universiteit Amsterdam Johannes Hölzl, Vrije Universiteit Amsterdam Robert Y. Lewis, Vrije Universiteit Amsterdam Assia Mahboubi, Inria Rennes – Bretagne Atlantique Freek Wiedijk, Radboud Universiteit Nijmegen |

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.

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. A recent
debacle is Fasel's proposed solution to Murthy's conjecture: it passed peer
review and was published in the prestigious Annals of Mathematics, before it
emerged that a lemma is flawed and the entire proof collapsed. 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.

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.

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 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. Especially for a young system, close cooperation between developers and users is essential.

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 proof assistant 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, 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. Conveniently, Formal Abstracts uses Lean as its lingua franca.

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 unappealing and 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.

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 mathematical components.

The design of formal mathematical libraries poses many scientific and practical challenges.

*Usable design*: The experience with building large formal libraries such as the Coq Mathematical Components 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. A challenge will be to find out how to exploit these new possibilities.

The libraries will be developed with maintainability in mind, so that they can serve in future research. To ensure their longevity, we will initiate a repository of third-party Lean formalizations and tools, inspired by the Archive of Formal Proofs.

Our goal is not only to prove lemmas and theorems but also to verify algorithms, such as those presented in Cohen's textbooks, and use verified algorithms to check entries in online databases such as the LMFDB. Beyond their intrinsic appeal, the algorithms often arise naturally in proofs—for example, proofs of decidability can be carried out by exhibiting a verified algorithm. Moreover, verified algorithms can be used to prove lemmas using reflection.

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.

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. As a young system,
Lean is an ideal testbed for new ideas. A strong reconstruction tactic based
on a procedure for first- or even higher-order logic is critical to
automation. The existing `super` tactic is unfortunately orders of
magnitude too slow to be useful. Developing a monadic prover with efficient
data structures and finding solutions to speed up the execution of
metaprograms will require innovative ideas.

We also want to contribute to the Lean simplifier's support for arithmetic and the envisioned algebraic normalizer, based on our experience working towards the first two objectives. 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, and veriT. 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.

Robert Y. Lewis (VU Amsterdam, postdoctoral researcher)

Johannes Hölzl (VU Amsterdam)

Assia Mahboubi (Inria Nantes)

Freek Wiedijk (RU Nijmegen)

Leonardo de Moura (Microsoft Research)

Femke van Raamsdonk (VU Amsterdam)

Pablo Le Hénaff (École Polytechnique Paris)

Casper Putz (VU Amsterdam)

Jens Wagemaker (VU Amsterdam)

The project is thankful for the support and advice of the following friends and colleagues: Peter Boven, Wan Fokkink, Cristiano Giuffrida, Kris de Jong, Mojca Lovrencak, Rikkert Stuve, Susanti Tang-Budiwandojo, and Caroline Waij.

**Lean Together 2019**

7–11 January 2019, Amsterdam, The Netherlands

Please write to Jasmin Blanchette for queries related to the project.

We are looking for outstanding candidates for postdoctoral, PhD, and intern
positions due to start between 2019 and 2021. Candidates should ideally have
some experience with interactive theorem proving *or* number theory and
be at ease with theory and engineering. Please contact Blanchette for more
information.