Custom Agent for Issue Generation

Stream: Formal conjectures

[Franz Huschenbeth]

I have created a custom Agent for Issue Generation for the Formal Conjectures Repo.

Features:

• Runs on Claude Agent SDK
• Takes URL or prompt as entry point
• Can do web searches for information
• Custom Tool: Checks if conjecture is already a open issue (fuzzy) or if it is in formal-conjectures code (fuzzy)
• Custom Tool: Checks prerequisites of mathlib (via loogle API) and gives a 0-5 formalizibility rating based on the current infrastructure (might need improvement I gotta check more)
• Custom Tool: Gives AMS Codes (with just the codes taken from the AMS PDF)
• Creates a issue.md (for now) and report.md detailing if the conjecture was duplicate or not
• Costs around 0.1$ per Conjecture (Running on Claude Haiku 4.5)

Future Ideas:

• Autoposting of the Issue to the Repo
• Take PDF (Books) as entry points (Have to check that)

You can view a few of the issues he created in the recent issues (for example #1795), I have copy and pasted them manually and checked them and indicated the AI usage at the bottom.

Motivation: If we can create more issues, we can identify easy to formalize issues. Also the information in the issue can be used as a entry point for a human / autoformalization agent to formalize the conjecture. Also reduces the bottleneck of creating issues to simply getting entry points (such as urls).

One question I have is, if I can also open Issues via the Github API (I would still review them), but I dont want to just spam them, so I thought to ask here first.

I am open for discussions and questions.

[Moritz Firsching]

Thanks! Seems like a good idea.
Looking through the issue, they seems it produces mostly useful output.
For one conjecture the check if it already exists in the repo failed (Hadamard, FC#1796).
It is not entirely clear to me if it is a good idea to open issue for conjectures which are still very far away from being able to be formalized in mathlib (like 4/5 or 5/5 in the rating generated). When they are in on of the problem list (like Hilbert, Wikipedia, etc, it is still great to add them) -- and I think all of the issues you opened are of that kind, thanks! If we add lot of hard issues like this we should introduce a label with a name like "requires much work" (other ideas?) or something, so people looking for issue they can work on can easily filter them out. (Of course over time, when Mathlib gets bigger, those labels could be removed for problems that can then be stated more easily. )

Re: Autoposting, i.e. using Github API versus manually: Probably doesn't make much of a difference, still important to review manually before posting in any case.

Instead (or in addition to) of taking Books as entry points one could also consider taking (recent?) arxiv papers (using latex source that is available for most arxiv paper directly is likely even slightly easier on the agent):
Let the agent figure out if there are any conjectures in the paper and if there are (and if they are simple enough to formulate them in mathlib, then make an issue for those. This will probably only extract a conjecture single digits percent of all papers, but those would be potentially very interesting material. If they are recent it would have the additional advantage that the authors of the papers would potentially be responsive when questions during formalisation of the conjecture arise.
Thank again!

[Franz Huschenbeth]

I have gone ahead and taken the list of wikipedia algebra problems to test how good it works (because it included duplicate open issues, duplicate formalized and no issue, the dedup tool got everything right for now). About the Hadamard Duplicate I wrote you at FC#1796.

I do agree that opening these hard issues is not entirely useful atm, beyond just having them tracked. Yeah a label sounds good, I could also add them automatically, if I get the rights to add labels. So like 0-2 "good first issue" 4-5 "Need significant infrastructure from Mathlib".

Good idea about the arxiv papers, will probably look into adding that next.