Machine-checked, machine-generated or machine-verified proofs

Automated deduction, also called automated theorem proving, is the generation of proofs of mathematical statements by computer programs. Some proofs can be built automatically by computer programs, while others require human assistance but are verified by software.

External resources