Computer-Assisted Proofs in the Arithmetic of Quadratic Forms - IPAM at UCLA

Explore a 47-minute lecture on computer-assisted proofs in the arithmetic of quadratic forms presented by Johnathan Hanke of Princeton University at IPAM's Machine Assisted Proofs Workshop. Delve into the historical context of quadratic forms and their computational challenges across various areas of modern mathematics. Examine simple theorems made possible through custom software implementations, taming the complexity of proofs. Follow the progression from basic definitions and equivalence of quadratic forms to advanced topics like local-global principles, Siegel's formula, and modular forms. Gain insights into proof tactics including Eisenstein lower bounds, cusp form upper bounds, and finite enumeration. Conclude with an exploration of ingredients necessary for formal proofs in quadratic forms.

Intro
Overview
Definitions of Quadratic Forms
Equivalence of Quadratic Forms
Classical Questions in Quadratic Forms
Numbers Represented by a (PDIV) QF
General Local-Global Principle
Quantitative Local-Global and Siegel's Formula
Understanding Theta Series Coefficients
Modular Forms
Tactic Part 1: Eisenstein Lower Bounds
Cusp Form Upper Bounds
Tactic Part 3: Finite Enumeration
4. Ingredients in a Formal proof of Q(Z)?