I'm more interested in the techniques used to generate these proofs, and how they can be improved to be as reliable at solving a broader class of problem than already formalized mathematical conjectures.