Yes, you are right, I am referring to the free loop space. I edited the "free" into the question.

First one needs a good strategy how to store statements. One this is defined the aggregating process and linking by ML and the user friendly search engine frontend can be independent and more and more improved over the years.

I am aware that there is sometimes no unique formulation of a theorem. That is not a problem. A perfect system/database would try to just capture exactly in a machine-readable form how a textbook states a theorem. Using some ML one then aggregates similar statements (the "same") theorems and displays them in a frontend view. Maybe listing the most stated version first and referring to other formulations etc.

So far I just found articles either analyzing existing systems or abstractly sophisticating about properties that a perfect library should have. Do you know about a recent concrete effort of building a perfect system? And can you give me a link for that IMU effort? Sounds interesting.