I’m really interested in AI4MATH, as I believe it will eventually replace me.

I'm working on a mathematical knowledge base software.

It's kinda like a local Github for math. In fact the backend is actually a Forgejo instance, I'm building a frontend for human and also a harness for agents that automatically consumes the knowledge base and expand on it. I realized the Issue/PR/review workflow works well for maintaining knowledge base too.

The motivation is actually help mathematicians/me TODAY to able to do math together with human/AI.

The knowledge base keeps mathematical writing as plain Markdown, but adds stable IDs, backlinks, search, draft changes, review, approvals, and merge. The agent side can read the same pages, follow the same references, propose edits, and go through the same review process as a human.

I’m not using formalization here. Everything is still natural-language proofs. The practical reason is that many areas I care about are not easy to formalize yet because it is not in mathlib.

I see this as a transition project: useful before autoformalization really works well, and maybe still useful afterward as the place where humans and agents organize exploration.