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.