Recorded 16 February 2023. James Davenport of the University of Bath presents "How to prove a calculation correct?" at IPAM's Machine Assisted Proofs Workshop. Abstract: How might one prove a calculation correct. The usual approach is to prove the algorithm correct, prove that the implementation (if different) is a correct implementation of the algorithm, and then the calculation by this algorithm/implementation is correct. However, it may not be possible to prove that the algorithm is correct, or that the implementation is correct. In this case, an alternative is for the implementation, while performing the calculation, to produce enough intermediate information that a proof engine, using these as hints, can then construct a proof of correctness of THIS calculation, rather than correctness of the general algorithm/implementation. We discuss this methodology in the context of real algebraic geometry (i.e. NRA in SMT-language). Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/