1. (toán), một kiểu lập luận xuất phát từ giả thiết, dùng suy diễn lôgic chặt chẽ để đi đến kết luận. Có nhiều phương pháp CMĐL như: chứng minh trực tiếp (xuất phát từ giả thiết đi đến kết luận), chứng minh bằng phản chứng (xuất phát từ phủ định của kết luận đi đến phủ định của giả thiết) (x. Định lí), chứng minh bằng quy nạp (x. Quy nạp toán học).

2. (tin học), một hướng nghiên cứu của tin học nhằm dùng máy tính để tự động hoá việc chứng minh các định lí trong một lí thuyết toán học hay trong một hệ hình thức nói chung. Có hai cách tiếp cận đối với việc CMĐL tự động: tìm kiếm tự động một chứng minh cho một định lí cho trước; suy diễn tự động từ một hệ tiên đề để tìm ra những "định lí" chưa biết trước.