Formalizing O-minimality
Reid Barton, University of Pittsburgh
9:30-10:15
Slides: pdf, video: YouTube
O-minimal structures are a particular kind of setting for "tame topology" with roots in real algebraic geometry and model theory. This talk will give an introduction to the subject and discuss the particular difficulties that arise in its formalization.
Generating Mathematical Structure Hierarchies Using Coq-ELPI
Cyril Cohen, Inria
10:15-11:00
Slides: pdf
In this talk we describe an ongoing work which purpose is to generate hierarchies of mathematical structures from annotated sets of axioms. The work is carried out on top of Coq using a plugin to meta-program using the lambda prolog interpreter ELPI. We provide a high level interface to instruct how to package together the appropriate axioms and we focus on how to make the use of such generated code robust to changes.
This is joint work with Kazuhiko Sakaguchi and Enrico Tassi.
Automating Asymptotics in a Theorem Prover
Manuel Eberl, TU Munich
11:30-12:15
Slides: pdf, video: YouTube
I will present the ‘real_asymp’ method, a recent addition to the repertoire of domain-specific automation in Isabelle/HOL that can solve many asymptotic questions (such as limits and ‘Big-O’ statements) about a large class of real-valued functions (almost) automatically in many cases. The method is a proof-producing Standard ML procedure that computes multiseries expansions, similar to the approaches taken by computer algebra systems like Maple and Mathematica. The method is fast enough to handle complicated problems arising in the formalisation of actual mathematics, and it has been tremendously helpful in automating away tedious tasks in our formalisation work.
On a Mathematician's Attempts to Formalize his Own Research in Proof Assistants
Sébastien Gouëzel, Université de Nantes
12:15-1:00
Slides: pdf, video: YouTube
I am mainly a mathematician, but I have been interested in proof assistants in the last few years. As a mathematician, I study among other things random walks on Gromov-hyperbolic groups, a fairly specialized subject which requires a huge body of results to be even defined. I have worked in Isabelle and Lean towards the (unrealistic) goal of being able to formalize my results in this area. I will report on these attemps, focusing on three interesting examples that have taught me three different lessons: the Morse lemma in hyperbolic geometry, the Bonk-Schramm embedding theorem, and the Gromov-Hausdorff distance. Knowing the maths is not a prerequisite for this talk.
Numerical Proofs in Nonlinear Control
Sicun Gao, University of California, San Diego
2:30-3:15
Slides: pdf
We can consider dynamical systems as loops over continuous time and Lyapunov functions as loop invariants. Nonlinear control design is thus a form of program synthesis that involves the search of numerical proof certificates. This approach is practical for many challenging nonlinear systems. In fact, by solving quantified formulas over the reals, we can find controllers that are more provably-robust than what can be obtained through standard optimal control methods. In particular, this approach opens up the possibility of using very expressive function approximators such as neural networks as proof certificates, and various statistical learning methods become relevant.
Towards an Optimizing Compiler for Numerical Kernels
Eva Darulova, Max Planck Institute for Software Systems
3:15-4:00
Slides: pdf, video: YouTube
Computing resources are fundamentally limited and sometimes an exact solution may not even exist. Thus, when implementing real-world systems, approximations are inevitable, as are the errors they introduce. The magnitude of errors is problem-dependent but higher accuracy generally comes at a cost in terms of memory, energy or runtime, effectively creating an accuracy-efficiency tradeoff. To take advantage of this tradeoff, we need to ensure that the computed results are sufficiently accurate, otherwise we risk disastrously incorrect results or system failures. Unfortunately, the current way of programming with approximations is mostly manual, and consequently costly, error prone and often produces suboptimal results.
In this talk, we present the current state of the tool Daisy which approximates numerical programs in an automated and trustworthy fashion. Daisy allows a programmer to write exact high-level code and generates an efficient implementation satisfying a given accuracy specification. We discuss Daisy's verification techniques for bounding the effects of numerical errors, and the approximations Daisy can synthesize fully automatically.
Higher Algebra in Homotopy Type Theory
Ulrik Buchholtz, TU Darmstadt
4:30-5:15
Slides: pdf, video: YouTube
One appealing application of homotopy type theory to mathematics is to the study of higher groups and related higher algebraic structures. These have simple definitions in terms of homotopy types; for instance, a k-symmetric n-group is the n-truncation of a k-fold loop type. Thus, the development of their theory is greatly simplified in homotopy type theory/univalent foundations as compared to other approaches. I'll sketch how much of the theory has been developed so far (some of it in joint work with Floris van Doorn and Egbert Rijke), and discuss the prospects for developing other areas of higher algebra.
Using Lean for New Research
Neil Strickland, University of Sheffield
9:30-10:15
Slides: pdf, video: YouTube
Associated paper: arXiv
Github repository: here
I recently released the paper "Iterated chromatic localisation" (jointly authored with Nicola Bellumat) together with a Lean formalisation of about 25% of the mathematical content. I will discuss this project, and the infrastructure and ecosystem that would be needed to make it convenient and useful for people to do this sort of thing routinely.
Reasoning with Non-linear Formulas in Isabelle/HOL
Wenda Li, University of Cambridge
10:15-11:00
Slides: pdf, video: YouTube
Reasoning about non-linear systems is hard, and it is even more tricky to do it within a proof assistant. In this talk, I will introduce an ongoing effort to bring cylindrical algebraic decomposition (CAD) to Isabelle/HOL. As one of the leading tools to reason first-order theory over the reals, CAD has been widely implemented in various systems including Mathematica, Maple, Z3 and Yices. However, to safely invoke the tool within a proof assistant, we need to justify its correctness within the logic. Though the journey is not yet finished, it has already resulted in some by-products, including verified procedures to reason algebraic numbers, real and complex roots of polynomials.
The Poincaré-Bendixson Theorem in Isabelle/HOL
Fabian Immler, Carnegie Mellon University
11:30-12:150
Slides: pdf, video: YouTube
The Poincaré-Bendixson theorem is a classical result in the study of (continuous) dynamical systems. Colloquially, it restricts the possible behaviors of planar dynamical systems: such systems cannot be chaotic. In practice, it is a useful tool for proving the existence of (limiting) periodic behavior in planar systems. The theorem is an interesting and challenging benchmark for formalized mathematics because proofs in the literature rely on geometric sketches and only hint at symmetric cases. It also requires a substantial background of mathematical theories, e.g., the Jordan curve theorem, real analysis, ordinary differential equations, and limiting (long-term) behavior of dynamical systems. We present a proof of the theorem in Isabelle/HOL and highlight the main challenges, which include: i) combining large and independently developed mathematical libraries, namely the Jordan curve theorem and ordinary differential equations, ii) formalizing fundamental concepts for the study of dynamical systems, namely the 𝛼,𝜔-limit sets, and periodic orbits, iii) providing formally rigorous arguments for the geometric sketches paramount in the literature, and iv) managing the complexity of our formalization throughout the proof, e.g., appropriately handling symmetric cases.
Formalizing a Sophisticated Definition
Patrick Massot, Université Paris-Sud
12:15-1:00
Slides: pdf, video: YouTube
Lean files: deps.lean, my_groups.lean
Data: groups_and_real_pruned.gephi, perfectoid_pruned.gephi
In this talk I'll try to explain what it means to formalize a sophisticated definition, using mostly the example of perfectoid spaces that I formalized in Lean with Kevin Buzzard and Johan Commelin. Then I will show examples where the peculiarities of type theory and formal proofs initially looked like a nuisance to us, but actually led us to improve a mathematical story. I will not assume familiarity with perfectoid spaces or any other mathematical topic beyond the basics of general topology.
A Coq Formalization of Lebesgue Integration of Nonnegative Functions
Sylvie Boldo, Inria
2:30-3:150
Slides: pdf, video: YouTube
Formalizing the mathematical notion of integration and the associated results in a proof assistant provides the highest confidence on the correction of numerical programs involving the use of integration, directly or indirectly. We focus on the Lebesgue integral, that is considered as perfectly suited for use in mathematical fields such as probability theory and real analysis. In this talk, I will present a Coq formalization of sigma-algebras, measures, simple functions, and integration of nonnegative measurable functions, up to the full formal proofs of the monotone convergence theorem (or Beppo Levi Theorem) and the Fatou-Lebesgue Theorem.
This is joint work with François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero.
Statistical Model Checking of Stochastic Hybrid Systems with Logic-Based Specifications
Geir Dullerud, University of Illinois
3:15-4:00
Video: YouTube
The presentation will focus on a simulation and computational approach to formal verification of the hybrid mathematical models that are formed when combining physics-based models, with discrete-transition models such as those which model software algorithms. Namely, the mathematical models that arise when for instance considering Cyberphysical Systems, or the Internet-of-Things. In many game theory, filtering problems and verification problems it is not possible to analytically obtain solutions for statistical properties of systems under study. We present a new verification algorithm for continuous-time stochastic hybrid systems, whose specifications are expressed in metric interval temporal logic (MITL), by deploying a novel model reduction method. By partitioning the state space of the hybrid system and computing the optimal transition rates between partitions, we provide a procedure to both reduce the system to a continuous- time Markov chain, and the associated specification formulas. We prove that the unreduced formulas hold (or do not) if the corresponding reduced formula on the Markov chain is robustly true (or false) under certain perturbations. In addition, a stochastic algorithm to complete the verification has been developed. We have extended the approach of this algorithm, and have developed a direct stochastic algorithm for statistically verifying a certain hybrid system class, and applied this technique to an extensive benchmark problem with realistic dynamics. Also discussed will be recent work on the use of negative correlation in model checking.
Deep Learning for Theorem Proving
Markus Rabe, Google Research
4:30-5:15
Project page: deephol.org
I will summarize recent efforts in machine learning for automated reasoning and the work of the N2Formal research group at Google. Our mission is to build an artificial mathematician, one that can understand natural mathematics found in scientific articles and books, and translate it to formal representations. So far, we have built a machine learning environment based on the interactive theorem prover HOL Light and a neural theorem prover called DeepHOL. Given a statement to prove, DeepHOL automatically selects appropriate premises and tactics, just like a human mathematician would. Training DeepHOL using imitation and reinforcement learning already achieves state-of-the-art performance in higher-order reasoning.
First-Order Theorem (Dis)proving for Reachability Problems in Verification and Experimental Mathematics
Alexei Lisitsa, University of Liverpool
9:30-10:15
Slides: pdf, video: YouTube
In this talk we introduce and overview conceptually simple but powerful and efficient method for solving reachability questions. The method utilises modelling of reachability between the states of a system by derivability in the classical first-order logic. With such a formalization (non-)reachability can be established by automated (dis-)proving using available automated reasoning methods and tools. We illustrate the method by the applications to the verification of infinite state and parameterized systems, and to the exploration of open mathematical problems, such as Andrews-Curtis conjecture in combinatorial group theory.
SMTCoq: Coq Automation and its Application to Formal Mathematics
Chantel Keller, Université Paris-Sud
10:15-11:00
Slides: pdf, video: YouTube
SMTCoq is a plugin for the Coq interactive theorem prover to work in conjunction with automated theorem provers based on Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT), in an efficient and expressive way.
A first objective of SMTCoq is to formally establish, in a proof assistant, mathematical results relying on large combinatorial properties that require automatic Boolean reasoning. To this end, the huge SAT proofs coming from such problems can be safely checked in Coq and combined with standard mathematical Coq developments in a generic and modular way. As a case study, a formal proof of the Erdős Discrepancy Conjecture was established.
A second objective of SMTCoq is to offer more automation to Coq users. To this end, Coq goals can be encoded and discharged to external, automatic provers that, as in the previous application, should output a proof that will be checked in Coq. The current distribution of SMTCoq thus provides new decision procedures that can be seen as a combination of existing decision procedures. An ongoing project is to improve the automation provided by SMTCoq, in particular by designing a small-step, modular encoding from Coq logic into first-order logic. Eventually, it will provide automatic tactics that can handle the "easy" reasoning under the scene, leaving the user with the mathematical and inductive reasoning only.
The heart of SMTCoq is a certified, efficient and modular checker for SAT/SMT proof certificates, expressed in a format that can encompass most aspects of SMT reasoning. Preprocessors - that need not be certified - for proof traces coming from the state-of-the-art SMT solvers CVC4 and veriT and SAT solvers zChaff and Glucose are implemented. Coq can thus work in conjunction with widely used provers.
Formal Methods and the Chromatic Number of the Plane
Marijn Heule, Carnegie Mellon University
11:30-12:15
Slides: pdf, video: YouTube
Today’s satisfiability solvers can not only determine whether a propositional formula can be satisfied, but they can also produce a certificate in case no satisfying assignments exists. These certificates, known as proofs of unsatisfiability, can be used for multiple purposes ranging from checking the correctness of the unsatisfiability claim to computing interpolants. In this talk, we focus on another application of proofs of unsatisfiability: computing an unsatisfiable core of the formula. The size of proofs tends to correlate to the size the corresponding unsatisfiable cores: the smaller the proof, the smaller the unsatisfiable core. We present a method to exploit this relation by computing a smaller and smaller proof of unsatisfiability to compute a small unsatisfiable core. We apply this method to improve the upper bound of the smallest unit-distance graph with chromatic number 5, which is currently a Polymath project. The method was crucial to obtain the best known bound of 510 vertices.
Integration of General-Purpose Automated Theorem Provers in Lean
Gabriel Ebner, TU Wien
12:15-1:00
Slides: pdf, video: YouTube
The sledgehammer tool in Isabelle is one of the most mature and most widely known approaches to integrate automated theorem provers such as Vampire or E in an interactive proof assistant. Similar hammers have also been developed for other proof assistants, such as HOLyHammer for HOL Light and CoqHammer for Coq. In this talk I will present ongoing work implementing such a hammer for Lean. Some features of Lean pose unique challenges, such as the expressive and ubiquitous type class mechanism. I will also present preliminary experimental results.
Lean 4: State of the ⋃
Sebastian Ullrich, Karlsruhe Institute of Technology
9:30-10:15
Slides: pdf, video: YouTube
This is a progress report on the ongoing work on Lean 4, the next version of Lean.
A Formal Proof of PAC Learnability for Decision Stumps (contributed talk)
Koundinya Vajjha, University of Pittsburgh
2:30-3:00
Slides: pdf, video: YouTube
Metamath Zero, or: How to Verify a Verifier
Mario Carneiro, Carnegie Mellon University
4:30-5:15
Slides: pdf, video: YouTube
As the usage of theorem prover technology expands, so too does the reliance on correctness of the tools. Metamath Zero is a verification system that aims for simplicity of logic and implementation, without compromising on efficiency of verification. It is formally specified in its own language, and supports a number of translations to and from other proof languages. In this talk I will talk about the various parts of the language and how they all fit together to solve the problem of bootstrapping trust into a theorem prover. Ultimately, we intend to use it to verify the correctness of the implementation of the verifier down to binary executable, so it can be used as a root of trust for more complex proof systems.
Polynomial Rings with Operators in Coq (contributed talk)
William Simmons, Hobart and William Smith Colleges
9:30-10:00
Slides: pdf, video: YouTube
Polynomial rings equipped with operators are useful for studying the formal theory of differential and difference equations, among other things. I'll discuss ongoing work in Coq on a general framework for such polynomials. The project uses the Mathematical Components library and SSReflect proof language, but aims be compatible with multiple formalizations of ring theory.
ForTheL as a Controlled Natural Language for Lean
Peter Koepke, University of Bonn
10:00-10:30
Slides: pdf, video: YouTube
At the Big Proof conference in May 2019 Tom Hales proposed to develop a Controlled Natural Language (CNL) for the Lean proof assistant in order to make formalizations and fabstracts naturally readable for mathematicians without the need to acquire the language of Lean. We are currently investigating whether the CNL Formula Theory Language (ForTheL) which in the the Naproche-SAD project is parsed into first-order logic, can also be faithfully translated into dependent type theory or Lean. Based on some promissing initial results I shall survey aspects of the natural language of mathematics and ForTheL and present parsing procedures, especially into type theory.
A Database of Definitions
Luis Berlioz, University of Pittsburgh
2:00-2:15
Slides: pdf, video: YouTube
Continuum Hypothesis
Jesse Han, University of Pittsburgh
2:20-2:45
Slides: pdf, video: YouTube
Tactics
Floris van Doorn, University of Pittsburgh
2:45-3:15
Source code: lean, video: YouTube
Controlled Natural Language
Thomas Hales, University of Pittsburgh
3:15-4:00
Video: YouTube
The Future of Mathematics?
Kevin Buzzard, Imperial College London
University of Pittsburgh Colloquium, Frick Auditorium
4:30-5:30
Slides: pdf
Mathematics is currently mostly done by humans, and the published literature is mostly correct. Is this good enough? ArXiv enables mathematicians to distribute their unrefereed research around the world very effectively, and citations of ArXiv papers in other ArXiv papers is certainly acceptable in our culture. But we cannot be 100% sure that the latest paper in the p-adic Langlands Philosophy is correct. Such a paper will surely have no practical real-world application, so if it is also not correct, then one might argue that it is worthless. Computer proof checkers offer a completely different way of doing mathematics, which is an area has no problems with accuracy but instead has a completely different set of problems. Computers can beat humans at chess and at go. Will computers one day be able to beat humans at theorem proving? Should we be teaching math undergraduates to use computer proof checkers? I am a number theorist by training, but have spent the last two years learning about computer proof checkers; I will give an overview of the area. No background in computer proof checkers or the p-adic Langlands philosophy will be assumed. The talk will be suitable for undergraduates.