I’m here to make software that everyone can use to learn and apply mathematics, and I’ll put it directly on the Web. I’m taking inspiration from work done on software verification using Type Theory and Logic Programming, and I have experience using Agda, modified for Homotopy Type Theory, to express abstract mathematical theorems in a programming language. Similar languages and techniques are well-within my grasp, especially those which are conscious of a foundation in Category Theory.I believe that human users and AI “bots” can work together on a network to solve real-life mathematical problems, and that developing a platform capable of problem solving at scale will be essential to research in all technical disciplines from the 21st century on.I’m looking for companies and engineers who are interested in similar projects – hopefully we can work together and learn from each other!I studied mathematics in the United States and in China. I want to learn more about the challenges of managing large collections of formalized information, including searching without knowledge of technical terms, proof discovery/suggestion, adaptive organization of the knowledge base, and the use of semantic interpretations to suggest new paths of inquiry. I believe that software engineering best practices for designing software libraries will be very relevant here.