[boroboro4]

It does, but not necessary with LLMs, see https://news.ycombinator.com/item?id=41069829 for example - this is mixing Lean with neural network to automatically proof theorems.