Title: Computer Aided Reasoning in Statistics
Abstract: Computer Aided Reasoning (CAR) uses a computer program to assist with mathematical reasoning. Proofs done in a proof assistant program are done formally, every step and inference is validated back to the axioms and rules of inference. Thus we have higher confidence in the correctness of a formally verified proof than one done with the traditional paper-and-pencil technique. Computers can track many more details than can be done by hand, so more complicated proofs with more cases and details can be done in CAR than can be done by hand, and proof assistant programs can help fill in the gaps in a proof. We give a brief overview of the proof assistant program HOL Light, and use it to formally prove the Markov inequality with an expectation based approach.