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.
It was not meant to be a serious comment even though it seems it may have touched a nerve.
Programming in Lean?
lol
Of course i agree they will be better--I'm happy to be like chess players and just admire the machines and entertains humans