If one of the lessons of LLMs was that much of "common sense" is covered in the written language corpus - that is, perhaps, basic human intelligence is covered

If one of the lessons of LLMs was that much of "common sense" is covered in the written language corpus - that is, perhaps, basic human intelligence is covered by language. Then, should we expect less with mathematics where written language is the normal way knowledge is propagated, and where formal proofs are wanted? An important distinction here is the coupling of search (not LLM for this one), a formal math language, and theorem proving. Math intelligence may not be merely the math written corpus, but adding the formal language and theorem proving sounds pretty powerful. All this still lacks self-directed goals. An intention. For now that's taken care of by the human asking questions.