I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.