8 ms·
> 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 th
by aleph_minus_one 6d ago
>
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/LANA_report_202607.pdf https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...
See also https://www.math.columbia.edu/~woit/wordpress/?p=15770 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/files/2026/07/Comments-on-the-LANA-Project-Report-of-Kato-et-al.pdf https://bpb-us-e2.wpmucdn.com/sites.arizona.edu/dist/4/404/f...