> It's also the first step in a new field of computer software that would augment mathematician's abilities and save them time It's a step, not the first step.

> It's also the first step in a new field of computer software that would augment mathematician's abilities and save them time It's a step, not the first step. Automated theorem generation has been published at least as far back as 1975, and it's been a field of interest since before the creation of the first computer.