Teraz, gdy wróciłem do Princeton po wydarzeniu inauguracyjnym expMath @DARPA, zaczynam zbierać myśli na temat przyszłości autoformalizacji, AI w matematyce oraz AI w nauce w szerszym kontekście. Oto, do czego doszedłem. "O produktywnych i nieproduktywnych tarciach"