feat(ErdosProblems): All 1179 Erdős conjectures formalized

[ryantuck]

All 1179 Erdős conjectures are now formalized

I have utilized Claude (primarily Opus 4.6) to produce formal conjectures for all 805 remaining Erdős problems, completing the formalization of the entire set of 1179 conjectures, and achieving Milestone 1: All open Erdős problems formalized in this repo.

I believe all conjectures adhere to the style guidelines in this repo and lake build does pass, making this a valid and nontrivial contribution to this project.

After contributing the conjecture for problem 13 I realized that formalizing the few hundred remaining conjectures basically boiled down to running a for-loop (and enough tokens to pay for it), so set out to accomplish just that.

Note that this PR contains no proofs, only formalizations of the conjectures.

Question for maintainers - how to proceed?

This is a massive PR generated exclusively by frontier AI and appears to be fairly new territory for this project. That being said, I've put significant effort into making it as ready as possible by focusing on strict adherence to style guidelines, believe it's worth the time to consider, and I'd be happy to assist in whatever way makes sense to do so.

Maintainers - Is this PR okay as-is? Should I open up 800+ PRs? Is there a more rigorous PR_REVIEW.md that Claude / Gemini / GPT can use to further review the conjectures to give the maintainers confidence that this isn't a deluge of AI slop? Does it make more sense to put that sort of proof-of-work in prior to merging, or do these appear correct-enough and would it make more sense to continue to apply a similar batch processing on all 1179 conjectures each time a new frontier model drops? Should I just go kick rocks and maintain my own repo?

Methodology

There were 374 formalized .lean conjectures in FormalConjectures/ErdosProblems/ when I began, leaving 805 of the problems in the set remaining to work on.

I utilized Claude in four separate stages for each problem in the batch:

1. Formalization - formalize conjecture - fetch from erdosproblems.com, implement, ensure lake build passes (see FORMALIZE_CONJECTURE.md)
2. Styling - update conjecture to adhere to repo style per guidance in AGENTS.md (see ADHERE_TO_DEEPMIND_STYLE.md)
3. Review - critical review of conjecture for adherence to 60-point CHECKLIST.md generated from AGENTS.md and README.md.
4. Fixes - apply fixes (if any) identified from review step.

The batch workflow I settled on for each stage ultimately was nothing fancy - essentially just opening up a tmux session on the server and leaving something like this running for days (lol):

$ cat todo-conjectures.txt | xargs -I % claude --dangerously-skip-permissions "Read FORMALIZE_CONJECTURE.md. Apply to problem %. Write output to conjectures/%.lean. Ensure `lake build` passes."

I did have to upgrade to a Claude Max subscription and hit my weekly token limit twice, so would've got this done sooner if I didn't have to wait around for that to reset. Additionally, I tried to parallelize the calls but that ended up torching through my per-session limit too fast, so I fell back on a very basic strategy of just processing the problems one at a time.

All compute was performed on a tiny e2-medium (2 vCPU, 4GB RAM) server in Google Cloud.

The repo containing the work done for this project is here: https://github.com/ryantuck/erdos-ai

[YanYablonovskiy]

I do believe the maintainers have access to latest ( and even in house Google ) AI tools that can do this for themselves if they like, the issue would be the reviewing -- which might persist here. But moreover it kind of defeats the point of the repository as a collaborative effort in my humble opinion ( and again it seems redundant because this can just be done by them without any open source input , simply the reviewer team and an AI can accomplish it, without ever opening individual issues, unless I am missing something ? )

[danielchin]

Speaking for myself, I'm not entirely opposed to AI generating all formalizations of problems that need to be formalized, though, doing this in batch like this makes it impossible for the maintainers to review. The reason why I'm not entirely opposed is because there's still a lot of problems to be formalized outside of the Erdos Problems.

I'll note a few things that caught my attention perusing through the changes:

1. You're redefining a lot of props that have already been defined before. In 190.lean, you're redefining HasMonoAP which is used in quite in a bunch of files already and I'm pretty sure already has a centralized location. Ideally, you should be reusing existing definitions.
2. The references are incomplete. I see a lot of examples of a citation using the author's name and the year with nothing about the journal or title. Some just have a citation (i.e., [Er89]) and that's it.
3. A good chunk don't have variants captured. Most of these are just the main theorems and not the additional text on the Erdos Problems website.
4. Some of these aren't super readable. Just randomly selecting one, 237.lean states ∀ M : ℕ, ∀ N : ℕ, ∃ n : ℕ, n ≥ N ∧ countRepresentations A n ≥ M), where it's more obvious to a human that it's a lim sup. If it were stated like limsup (fun n ↦ (countRepresentations A n : ℕ∞)) Filter.atTop = ⊤, it's probably more obvious.
5. A lot of the current open problems are not exactly the most formalizable (which is why I've been avoiding them for now) and probably requires discussion on how we should formalize them. For example 265 (https://www.erdosproblems.com/265), the question is how fast can $a_n \to \infty$ grow? Your formalization combines some of the alternative text and is trying to state a slightly different problem.

Obviously, let's hear what the maintainers have to say about this. But my general thoughts are, 1) this probably has to be broken into smaller PRs for review, 2) please don't open 800 PRs at once (we just had a fiasco yesterday of a rogue agent opening up 1000s of PRs and we probably don't want that again) if anything just release them like 10 at a time for maintainers to review, 3) there probably needs to be some human intervention involved to review, agree on readability, and confirm accuracy on these formalizations.

That being said, this is still a great starting point for some of the formalizations by getting pen on paper. It just needs a little bit more oomph to get it over the line.

[mo271]

Thanks @ryantuck!

Many things look good here.

Other comments already made some good points, but let me give a bit more of an explanation. Let's start with an example, the problem with the lowest number that is of status open and not yet in our repo is https://github.com/ryantuck/formal-conjectures/blob/22e7fa942bade2df459745d69ad9adce5235f71c/FormalConjectures/ErdosProblems/7.lean

In that file one can provide a trivial proof of the theorem you formalised:

 @[category research open, AMS 11]
theorem erdos_7 : answer(True) ↔
    ∃ S : Finset (ℤ × ℕ), IsCoveringSystem S ∧ HasDistinctModuli S ∧ ∀ p ∈ S, Odd p.2 := by
  norm_num(config := {singlePass:=1})[IsCoveringSystem,HasDistinctModuli]
  exact ⟨{(0,1)},by simp_all⟩

That shows that -- in this case -- some definition/formalisation of a statement is wrong.

That does not mean that all of the formalisations are mathematically incorrect, but the looking at the first open one in the list clearly has a bug. (I'm mainly looking at "open" conjectures, and I do expect that many of the "solved" ones are currently easier to formalise)

Some other aspect in general concern more the style, but it it not only about "how to format docstrings" but plays also into mathematical correctness:

• many concepts are defined multiple times, instead of only once and then re-using them from our ForMathlib. For instance in the example above, I suppose "covering system" is used in many problems, hence we would want to re-use that definition instead of (mis)formalising it every time
• More generally as much as possible from existing definitions from Mathlib and ForMathlib should be re-used. (In fact, coming back to the example there is already FormalConjecturesForMathlib/NumberTheory/CoveringSystem.lean, which potentially contains some useful stuff in this case. the limsup from some comment above is another example, and this seems a more general problem here.

I do think what you are doing is useful and welcome, I just want to make sure we can incorporate the suggested formalisations without introducing too many misformalisations.

Concrete suggestions how to move forward from here:

1. perhaps open ~10 pull requests, each with a single problem (preferably from the type research open) and we review it (then you could incorporate the collective feedback from that into making your pipeline better/postprocessing it!)
2. it should be ok and easy to review also groups of Erdős Problems when they are all concerning similar topics.
3. I will prepare a commit with "obvious" misformalisations such as the one described above, which is then in turn perhaps useful to tune the pipeline edit: commit here: a3168c3

Then 1. and 3. in turn can also be used to improve our AGENTS.md

Does that sound good?

I hope this really helps to finish of https://github.com/google-deepmind/formal-conjectures/milestone/1 faster, and we will make a good effort to review quickly enough...

[franzhusch]

I think that AI Agents are underutilized for this repository. This is part of the reason that I have advocated for a AGENTS.md (added by @Paul-Lez) and have created a custom Issue Generation Agent to alleviate the bottleneck of not knowing what problems we should formalize (or have already). I also did this with the potential thought of having a AI Agent take these issues as a entry point, so if your approach works works sufficiently we can also think about expanding it to general issues of this repo, instead of just the erdos problem website.

As with all software systems, also Agentic Systems are a iterative process. As @mo271 has pointed out, we can do this iteration and if our confidence in the AI Agent System increases, we can potentially increase the throughput.

I have read your CHECKLIST.md and FORMALIZE_CONJECTURE.md and they are mainly focused on stylistic guidelines, not on mathematicial correctness and @mo271 has already found one misformalization.

To increase the quality and alleviate the reviewer bottleneck further, I would suggest implementing a fourth check "Math Review", mainly oriented towards checking the mathematical correctness of the formalization. A rough overview, of what would be a sensible for this check:

• Read the Source Page and follow sources to gain a mathematical understanding of the problem
• Check if the formalized Lean statement is semantically equivalent to the natural language statement
• Try to find easy proofs to the problem, which would suggest a misformalization
• Add Category Test Statements of definitions if sensible

Furthermore I think it might be the most bang for the review buck, if you first create PRs for problems, which have a short formalization. But I like that you have gone ahead and implemented this idea and I hope it works good and if it does, one can potentially think about shifting the contributions of the open source community to reviewing the mathematical correctness of such formalization.

[mo271]

@ryantuck some discussion here: https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/How.20to.20proceed.20on.20.22All.201179.20Erd.C5.91s.20conjectures.20formalized.22/with/578080877

It would be great if we could turn this pull request into something useful!

[franzhusch]

I left some comments on the example PR that you shared here. @ryantuck

[ryantuck]

Good discussion so far, please feel free to reuse my results or start from scratch :)

Hello everyone, thanks for the input, glad this has sparked interesting discussion, lots of good points raised here. I really appreciate the feedback from @YanYablonovskiy @danielchin @mo271 @franzhusch.

Agree there are a few logistical hurdles in the way of getting the entire set of problems fully-formalized.

The last thing I want is for the existence of this PR to complicate, discourage, or delay further work on formalizing these problems, especially by those who are more steeped in the math than I am. I'm very pleased with having set out to do something ambitious and getting this far in the first place.

Therefore, given the not-quite-ready-to-be-merged nature of it in its current state, I'd be happy to close this PR and re-open a later one after a few more rounds of AI-powered refinement on a bulk set of problems.

Continuing AI pipeline refinements

I plan to continue hacking away at the AI formalization pipeline and improve the quality of the average formalization before submitting any subsequent PRs. Once these get a bit further along I will share the updates either in bulk form or in the suggested smaller batches of similar problems.

From the feedback, I've identified a handful of checks for Claude to focus on during an additional round of iteration.

I'm currently running all 800 problems through a pipeline that produces a detailed review of the current formalization and subsequently addresses those various fixes.

See below for details, and see ryantuck#1 for an example of doing so for problem 7, mentioned above. Initial results are encouraging - the model appears to be fairly thorough when assessing viability of formalization and critically reviewing completeness. (@franzhusch - I saw your feedback on this and appreciate the insights, will certainly adapt the code accordingly!)

I'm prompting the model with:

Read REVIEW_MATH.md. Produce a review of Erdos problem %. Put high effort into thinking. Utilize sub-agents as necessary. Be thorough.

And subsequently,

Read ai-review/%.md. Update the formalization based on the suggestions in that document. Be thorough. Run lake build for the whole project to confirm it builds successfully.

Review Math [Current Agent Prompt]

Assume the role of a PhD-level mathematician.

The goal is to review a particular Erdos Problem formalization (problem number NUM) to answer the following questions. Produce a review document called ai-review/NUM.md.

1. Code reuse - Can any code from the existing codebase be repurposed? Look in FormalConjecturesForMathlib to determine if an existing implementation would work just as well.
2. Citations - Fetch data from https://www.erdosproblems.com/NUM to ensure any citations included in docstrings are documented as they exist on the website as opposed to shorthand references.
3. Variants - Are all variants of the problem captured by the formalization?
4. Readability - Could the code be made more readable?
5. Formalizability - Is the problem as stated precise enough to be obviously formalizable? Provide an assessment of the ambiguity of the statement.
6. Correctness - Is the formalization as-implemented correct and complete from a mathematical perspective? Would an experienced mathematician identify any obvious flaws? Is any incompleteness or incorrectness attributable to ambiguity in the statement itself?

[danielchin]

A quick note on (2) in your current agent prompt. For citations and docstrings, it may be better to pull data from https://www.erdosproblems.com/latex/NUM instead. The citations are well formatted there and you can more or less copy and paste the docstrings from there as well (with some minor edits).

The one nit I've been getting from reviewers specifically for docstrings is to turn the latex special characters in names to the actual character (i.e., Erdős instead of Erd\H{o}s).

[ryantuck]

Breaking down to smaller PRs

As indicated in my last message and a couple hundred commits on this branch since then, I've processed all problems through two further stages: (1) review and (2) fix issues. I believe they're now as good as I'm going to get them using a pure AI pipeline and Claude Opus 4.6.

My goal is to now break this contribution down into a series of manageable PRs for review, and close this one out.

380 Open Problems

As discussed, Milestone 1 is focused on open problems.

I fetched the canonical dataset from the teorth/erdosproblems repo.

I took the union of the set of the 650 open problems listed there (as of 2026-03-16) and my 808 formalizations to get a list of 380 open problems with new AI formalizations.

Open Problems by Category

It was suggested that PRs would be more manageable if problems were grouped by category, so I had Claude conduct a review and it came up with the following:

>>> data = yaml.safe_load(open('open-erdos-problems-by-category.yml'))
>>> for category, problems in data.items():
...     print(category, len(problems))
... 
additive_combinatorics 42
analysis_polynomials 16
combinatorial_geometry 44
combinatorics_general 30
graph_theory 80
number_theory 124
probability_random 6
ramsey_theory 15
sequences_asymptotics 3
set_theory_infinite_combinatorics 20
>>> print(sum(len(problems) for problems in data.values()))
380

Three initial smaller PRs

I've opened three PRs for the categories with the lowest representation in the dataset to function as a starting point:

• sequences_asymptotics (3): feat(ErdosProblems): formalize 423, 839 #3586
• probability_random (6): feat(ErdosProblems): 6x probability-related formalizations #3587
• ramsey_theory (15): feat(ErdosProblems): 15x ramsey theory formalizations #3588

If this approach works well-enough, I'll point Claude at the problem of further breaking down to smaller problem sets for the larger categories.