Finding counter examples might be easier, but AI's also useful for assisting in creating proofs. For example, Anthropic just published a formalization of Fermat

Finding counter examples might be easier, but AI's also useful for assisting in creating proofs. For example, Anthropic just published a formalization of Fermat's last theorem a few days ago, something that human researchers have been working on for decades.