[dpbriggs]

This is more analogous to programmers working with copilot. There's an exciting possibility here of mathematicians feeding these systems subproblems to assist in proving larger theorums.

[highcountess]

It was not meant to be a serious comment even though it seems it may have touched a nerve.