Collaborative tools for the formal mathematics ecosystem human with human, human with agent, agent with agent.
Let your theorems, open problems, and strategies be shareable, workable, and citable.