»For mig at se er situationen klar,« skrev Patrick Massot, professor i matematik på Université Paris-Saclay, i en besked på Lean-projektets diskussionsside. »AI-virksomheder, og især Math, Inc., vil sønderbombe hele feltet og gøre det til en gigantisk radioaktiv ødemark, der aldrig vil kunne understøtte liv igen.«

Lean-projektet er et forsøg på at samle al vores matematiske viden og oversætte den til et logisk symbolsprog. Hvis man svedte over matematikken i gymnasiet, kunne man måske mene, at der i forvejen var rigeligt med formler og symboler. For Lean-folkene er det dog ikke nok. Når en matematiker beviser en sætning, bruger hun typisk en blanding af symboler og almindeligt sprog. I princippet kan den slags beviser formaliseres, det vil sige oversættes til et argument, der kun består af symboler. Den slags beviser er sikrere, fordi man ikke kan springe noget over, men de er også svære at lave, og derfor gør man det sjældent i praksis.