Six months inside the formal-reasoning community taught us that mathlib4 reviewers repeat the same notes across PRs. We wanted to know if those patterns were retrievable without an LLM. They are — this is that index, free for the community.
Paste a pull request diff or description. Returns the most relevant reviewer comments from closed mathlib4 PRs — no LLM, pure retrieval.
v0. Short queries are noisy, the index is a snapshot. Tell us what surprises you — founders@desargues.ai.
⌘↵