I think we need to start looking at another approach, can we create interactive reflex games that upload the knowledge from LLM's or perhaps domain specific ones for formal mathematics, so that mathematicians get a similar level of access to the domain of discourse as the LLM?