I'm dutch and not understanding his NL thesis, though i think these days its just as easy to let an ai provide a claim that is actually false, it be easier to hack lean then solve some of those solution for an AI