I believe if you need a human tutor to understand category theory or Lean then you don't have the requiste math/CS background, and a human/LLM tutor won't be able to meaningfully teach you anything.

Note I said "meaningfully" - something with LLMs that deeply concerns me is that they provide edutainment, and people actually think they're learning something. One of the comments on this thread mentioned giving a "dense linear algebra pdf" and having an LLM use the Socratic method. I guarantee they would have learned more if they read the PDF. I strongly doubt they learned anything at all with a bunch of silly "Socratic" questions about linear algebra. But it felt like they learned something!

" if you need a human tutor to understand category theory or Lean then you don't have the requiste math/CS background and a human/LLM tutor won't be able to meaningfully teach you anything."

What an incredibly elitist thing to say.

No, it's an honest thing to say. If you're not able to read a graduate-level textbook and teach yourself category theory then you don't have the mathematical maturity to understand category theory. You need to start smaller: ideally abstract algebra and point-set topology, or set theory and mathematical logic if you just want the CS applications. Likewise with Lean. Of course there is a place for a good human instructor. But mathematical maturity must be developed the hard way.

Even if you are correct, which you aren't, a good tutor almost ALWAYS helps people learn faster. This is just a really odd thing to argue.