Not sure this really holds: there is no symbolic LEAN type system in any animal brain as far as I can tell. I do think the point about the AI needs to sanity check is right. I imagine all this is will fall out from the visual, audio and other senses feedback loops though. I dont see the fundamentals needing explicit algebraic reasoning - that will surely come later.