Tekoäly pystyy nyt tuottamaan uutta mielenkiintoista matematiikkaa.
Mutta on paljon helpompaa tuottaa uskottavalta kuulostavaa hölynpölyä.
Olen huolissani siitä, että jälkimmäinen, jota käyttäjät kopioivat ja edistävät ilman matematiikan ymmärrystä, hukuttaa ensimmäisen.
Erdősin ongelmasivuston omistajana/ylläpitäjänä ketju, jossa on joitakin kommentteja tähän ratkaisuun #124:
1) Tämä on hyvä todiste, jonka tekoäly esitti muodollisesta lausunnosta ilman ihmisen osallistumista ja joka sitten virallistettiin Leanissa. Tämä on jo vaikuttavaa!
Olemme syvällisen muutoksen kynnyksellä matematiikan alalla. Tunnelman komennus on täällä.
Aristoteles @HarmonicMath:sta todisti juuri Erdos-ongelman #124 vuonna @leanprover, aivan yksinään. Tämä ongelma on ollut avoinna lähes 30 vuotta sen jälkeen, kun se on esitetty artikkelissa "Complete sequences of sets of integer powers" lehdessä Acta Arithmetica.
Boris Aleksejev ajoi tämän ongelman käyttäen Aristoteleen beta-versiota, joka on äskettäin päivitetty paremmaksi päättelykyvyksi ja luonnollisen kielen käyttöliittymäksi.
Matemaattinen superälykkyys lähestyy minuutti minuutilta, ja olen varma, että se muuttuu ja kiihdyttää dramaattisesti edistystä matematiikassa ja kaikissa riippuvissa aloissa.