> It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis.

People did attempt this:

https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...

See also https://www.math.columbia.edu/~woit/wordpress/?p=15770

Here are Kirti Joshi's comments about the LANA project report: https://bpb-us-e2.wpmucdn.com/sites.arizona.edu/dist/4/404/f...