Isabelle ML metaprogramming teaches automatic polynomial degree estimation
A First Introduction to Isabelle/ML Metaprogramming: Automatic Estimation of Polynomial Degrees
Logic in Computer Science
Summary
Figuring out how complicated a polynomial is by measuring its degree can be tricky, especially with many variables. The authors show how to use Isabelle/HOL, a tool for checking math proofs, to write a program that automatically finds an upper limit on these degrees and proves the result is correct. They focus on making a clear introduction for mathematicians new to programming in Isabelle’s ML language. Their example involves multivariate polynomials linked to specific number theory problems known as Diophantine pairs.
What this means in practice
- •For formal methods engineers: Automate the verification of polynomial properties within theorem provers to increase proof reliability and reduce manual effort.
- •For mathematical software developers: Incorporate automated polynomial degree estimation into proof-assistant-based tools for formalising mathematical problems involving multivariate polynomials.
Authors
Jonas Bayer, Anna Danilkin, Marco David, Annie Yao
Abstract
This article offers an introduction to metaprogramming in Isabelle/HOL for beginners, based on a running example for working with multivariate polynomials. The example is motivated by our formalisation of universal Diophantine pairs. We describe the implementation of the poly_degree command, which computes upper bounds on the total degrees of multivariate polynomials and automatically proves their correctness. The complete metaprogram handles a variety of special cases but herein we present a simplified version for the sake of exposition. We describe our development process and design decisions; our goal is to offer a small and self-contained tutorial on Isabelle/ML, for mathematicians who want to get started with metaprogramming.