Computing with or Despite the Computer - IPAM at UCLA

Explore the intricacies of computing class numbers of quadratic number fields through a thought-provoking lecture presented at IPAM's Machine Assisted Proofs Workshop. Delve into Anne Baanen's collaborative project, which formally verified computations as part of the Lean mathematical library. Compare and contrast three distinct approaches to computation: traditional paper-based methods, computer-assisted proofs using Lean, and rapid calculations with Sage. Examine the significant time disparities between these methods and consider the implications for mathematicians and computer scientists. Gain insights into the challenges and opportunities that arise when integrating different computational paradigms, and discover how this intersection creates novel questions in the fields of mathematics and computer science.