points
It's doing math proofs. At this point, it's fully clear that objective reality is that the LLM is not parroting anything here.
https://lean-lang.org