Computer-Assisted Proofs in the Arithmetic of Quadratic Forms

Johnathan Hanke
Princeton University

Since its early history, the ideas and results in arithmetic of quadratic forms have been inspired and often proved by explicit computations. While quadratic forms are one of the simplest non-linear objects one can study, the related computations needed to understand their properties can be quite involved and reach across many areas of modern mathematics.

In this talk we describe some simple theorems in the arithmetic of quadratic forms that have been made possible by the use of computers and related custom software implementations, which help to tame the complexity needed to prove them.

Back to Machine Assisted Proofs