Lemma

• 

Inspiration

Hi, my name is Bernabé, and this is my project, Lemma.

Over the past year, I’ve heard stories and read news about researchers—and even students—using AI to discover new proofs or make progress on long-standing mathematical problems, including some of the famous Erdős problems.

This is exciting and optimistic, but it also introduces a new challenge: as AI helps produce an increasing number of proofs, conjectures, and solutions, how will humans connect them into a coherent development of mathematics and science?

And, perhaps more importantly, what role will researchers play in that process?

Terence Tao recently published an insightful article exploring this topic, in case you want to go down that rabbit hole.

This is a complex question that the scientific community will need to address together. I don’t pretend to have the answer, but as a software engineer, I wanted to contribute through something I know how to build.

I had seen applications that use AI agents to solve mathematical problems and produce LaTeX documents. However, the result can quickly become a collection of messy, disconnected information—something similar to spaghetti code in software development.

Mathematical reasoning rarely follows a single, linear path. Researchers explore different strategies, reconsider assumptions, return to earlier decisions, and abandon dead ends. In a traditional AI conversation, that structure is easily lost, especially as the context grows.

That is why I created Lemma.

What it does

Lemma is an IDE-like collaborative workspace where humans and AI agents work on mathematical reasoning together.

Engineers, mathematicians, physicists, students, and anyone working with mathematics can use Lemma to define objectives, provide context, explore strategies, and develop solutions as structured reasoning graphs.

Instead of treating a solution as one long document or conversation, Lemma organizes it into objectives, strategies, branches, and individual reasoning steps. Users can interrupt the process at any moment, correct an agent, introduce a new idea, return to an earlier step, or create an alternative branch without overwriting the original path.

The core workflow is interrupt, branch, continue: a human changes the direction of a solution, and the agent reads the updated state through WebMCP and continues from there.

WebMCP is fundamental to this experience. Humans interact through a visual workspace, while agents can directly read and update the same structured reasoning graph. Both operate on the same source of truth, using the interface that works best for each of them.

Ultimately, Lemma is my approach to keeping humans in the loop—combining human creativity, context, and judgment with the speed and capabilities of AI to pursue mathematical goals together.

How we built it

Lemma is built as a TypeScript monorepo using pnpm workspaces.

The frontend uses React 19, Vite, strict TypeScript, React Router, XYFlow, and Dagre. XYFlow and Dagre power the visual reasoning canvas, where strategies, branches, dependencies, and mathematical steps are displayed as an interactive graph.

Mathematical content is written in Markdown with embedded TeX and rendered using react-markdown, remark-math, and KaTeX.

The backend is built with Supabase, using:

• Supabase Auth for authentication.
• PostgreSQL for the persisted reasoning graph.
• Row Level Security to protect each workspace.
• Realtime to keep the interface synchronized after changes.
• Storage for context files and supporting material.
• Edge Functions for the authenticated API and embedding pipeline.
• pgvector and full-text search for semantic step retrieval.

The reasoning graph is the source of truth. Entities such as workspaces, objectives, strategies, branches, steps, assumptions, sources, decisions, and results are stored as structured relational data instead of being inferred from a Markdown document.

The frontend, API, and WebMCP layer share the same Zod schemas, helping ensure that humans and agents interact with the same validated contracts.

At the top-level page, Lemma registers 22 WebMCP tools. These allow agents to inspect the workspace, create and update objectives, develop strategies, add steps and dependencies, create branches, mark assumptions or dead ends, compare branches, request human decisions, search previous reasoning, and generate a clean solution.

All agent mutations use the same authenticated application services as the visual interface. When an agent changes the graph, the result is immediately reflected and highlighted in the workspace.

The web client is hosted on Vercel, while Supabase provides the database and backend services.

Challenges we ran into

The biggest challenge was developing a clear mental model for structuring mathematical problems.

Mathematical reasoning is not simply a document, a chat, or a linear list of steps. I had to think carefully about which entities should participate in the process, how they should relate to one another, and how to preserve alternative paths without losing the history of the original reasoning.

Designing the interface was another major challenge. A reasoning graph can contain objectives, strategies, branches, steps, dependencies, assumptions, and results, so presenting all that information in a way that remains comfortable to navigate and understand was difficult.

I am happy with the current direction, but the interface could still be improved significantly as the conceptual model evolves and more people test it.

Accomplishments that we're proud of

I’m proud of having built a working prototype in record time that already allows mathematical problems to be explored in a visual and organized way.

There is still plenty of room to improve the problem-solving process, but one moment made me especially proud. A friend of mine who is studying mathematics tested Lemma and told me that he loved how easy it was to work with AI agents through the application.

That feedback made the idea feel real. It showed me that Lemma was not only an interesting technical experiment, but that its visual and structured approach could genuinely make AI-assisted mathematical reasoning easier to follow.

What we learned

The most important thing I learned was how people mentally approach mathematical problems.

Although I enjoy mathematics, it is still a hobby for me. Building an application intended to help people who are significantly better at mathematics than I am was challenging at first.

It forced me to think beyond the final answer and focus on the actual reasoning process: how ideas are introduced, how assumptions affect later conclusions, how different strategies emerge, and why returning to an earlier decision is such an important part of solving difficult problems.

I also learned that building effective tools for AI collaboration is not only about giving agents more capabilities. It is equally important to make their work inspectable, editable, and easy for humans to redirect.

What's next for Lemma

The next step is to improve Lemma’s conceptual model and introduce additional entities that support other types of mathematical work.

For example, Lemma could also be used as a learning environment, with dedicated explanation nodes that help users understand why a particular step works—not just what the next step is. There are many other possible workflows that could be built on top of the same reasoning graph.

I would also like to integrate tools based on Lean, allowing agents and researchers to translate results into formal proofs and mechanically verify whether a conclusion is correct. This could create a valuable bridge between exploratory mathematical reasoning and formally verified results.

Another feature I would love to create is a collaborative mode. Researchers could publish their work so that others could explore it, contribute new ideas or branches, and use previous research as a source of reference and context.

In the long term, Lemma could become more than a workspace for solving individual problems: it could become a shared, connected environment for developing, verifying, and communicating mathematical knowledge alongside AI.

Built With

• react
• supabase
• vercel
• vite