ACS Project Proposals by Prof L C Paulson

A wide class of possible projects involve formalising mathematics using the proof assistant Isabelle/HOL. Such projects will suit students who have a mathematical background, especially if they are already familiar with the theorems that they choose to formalise. There is an online list of 100 well-known theorems, and a separate list showing how many of these have been tackled. As of this writing, 86 of them had been formalised in Isabelle, making it the top system (tied with HOL Light). All the straightforward theorems may have been taken, but you can suggest anything from your own background.

Formalising Turán’s Graph Theorem in Isabelle/HOL

This theorem concerns the question

Suppose G is a simple graph that does not contain a k-clique. What is the largest number of edges that G can have?

Turán answered this question in 1941, giving an explicit formula. In Chapter 36 of Proofs from THE BOOK (which is free to download), five different proofs are presented. It's up to you to choose which is the most beautiful, or at least, the easiest to formalise! (Thanks to Angeliki Koutsoukou-Argyraki for this suggestion.)

The following project suggestions for 2021/22 are courtesy of Wenda Li, who would be happy to co-supervise.

Formalising Real Closed Fields (RCF) in Isabelle/HOL

The theory of RCF plays a pivotal role in both real algebraic geometry and computer algebra. RCF itself can be defined equivalently in various ways. The goal of this project is to formally prove Theorem 2.11. in Bochnak, Coste and Roy [1]: If R is a field then the following properties are equivalent:

R is real closed.
R[i] = R[T]/(T^2 + 1) is an algebraically closed field.
R has the intermediate value property.
R is a real field that has no non-trivial real algebraic extension, that is there is no real field R1 that is algebraic over R and different from R.

This project can start on top of the previous development of algebraically closed fields in Isabelle [3]. There has been a related development of RCF in Coq [2]. If time permits, the student can even proceed to prove the field of Puiseux series: an instance of a non-Archimedean real closed field.

Formalising Thom encoding in Isabelle/HOL

Real algebraic numbers are usually encoded as an univariate integer polynomial P and an interval (with rational end points) such that there is exactly one root of P within this interval. However, this encoding is not sufficient in the field of rationals extended with real algebraic numbers and infinitesimals, since a polynomial with infinistesimal coefficients can have roots that can be isolated with a rational interval. To addresss this problem, we may need Thom encoding to distinguish polynomial roots in a non-archimedean field as has been implemented in the Z3 SMT solver [4]. In the project, the goal is to formalise the fundamental property of Thom encoding in Isabelle/HOL (Proposition 2.28. in Bochnak, Coste and Roy [1]).

Extending linear arithmetic with non-linear reasoning

Linear problems like “x>2 ∧ y>1 ⟹ x+y>2” can be automatically solved with the linear arithmetic tactic linarith in Isabelle. The linarith tactic fails when a non-linear term arises: “y > 1 ⟹ x^2 + y >0”, but we can extend the linarith tactic by eliminating the nonlinear term x^2: “z≥0 ∧ y>1 ⟹ z+y >0”. This project aims for extending the linarith tactic in Isabelle for some non-linear problems. There have been similar tactics in Lean and in Coq, so we have a moderate start.

References

Bochnak, J., Coste, M. and Roy, M. F. (2013). Real algebraic geometry (Vol. 36). Springer.
Cohen, C. (2012, August). Construction of real algebraic numbers in Coq. In International Conference on Interactive Theorem Proving (pp. 67-82). Springer.
Paulo Emílio de Vilhena and L. C. Paulson (2020). Algebraically closed fields in Isabelle/HOL. In: Nicolas Peltier and Viorica Sofronie-Stokkermans (editors), IJCAR 2020
Grant Passmore and Leonardo de Moura {2013}. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. Proceedings in the 24th International Conference on Automated Deduction (CADE-24).