Recorded 14 February 2023. Anne Baanen of Vrije Universiteit presents "Computing with or despite the computer" at IPAM's Machine Assisted Proofs Workshop. Abstract: I have recently been collaborating on a project where we compute the class number of quadratic number fields, formally verified as part of the Lean mathematical library. This project took many orders of magnitude more time than the same computation on paper, while Sage finishes in one second. In this talk I want to discuss these three different views of computation and how making them cooperate can create interesting new questions for mathematicians and computer science. Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/