This is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the steps are correct. It doesn’t have any creativity (that’s up to the mathematician).
*I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.
*I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.