Marcus Barnes

The current pace of development in mathematics is incredible. Independent researchers and AI labs are formalizing large swaths of mathematical infrastructure. But there is one catch: understanding Lean does not always feel natural. After a period of preparation, I am excited to launch a new project, Agentic Approach to Computer Algebra Systems, generously supported by Renaissance Philanthropy through its AI for Math Fund 2026. The project will be shared between Adam Mickiewicz University and Warsaw University of Technology. Over the next two years, we will focus on building tools and experiences for mathematicians who want to work smoothly with AI agents and formalized mathematics without losing the flexibility of pen-and-paper exploration that they enjoyed so much in the past. For me personally, this is the start of a new adventure, where the challenge is very much like that of a start-up. We will build our solution in the ever-changing landscape of increasingly powerful AI agents. I believe there is still value in work done by mathematicians for other mathematicians. Let me know if you are interested in getting in touch, whether to collaborate or simply share some kind words, ideas, or opportunities to join forces on more cross-disciplinary projects.

I'm delighted to announce that I have received two years of funding from Renaissance Philanthropy to build an open-source agentic computer algebra system that will work with LLMs to support mathematicians in their research. Many thanks to the selection committee and the funders!