Fixing a sign error in Erdos 392

Stream: PrimeNumberTheorem+

[Terence Tao]

When reviewing the blueprint graph I noticed an oddity in the Erdos 392 project: the final theorems (erdos-sol-1, erdos-sol-2) were mysteriously disconnected from the rest of the Erdos 392 lemmas; and the (AI-provided) proofs were suspiciously short. After some inspection I realized the problem: I had asked to prove the (trivial) statements that $n!$ can be factored into at least $n-n/\log n + o(n/\log n)$ factors of size $\leq n$, and at least $n/2-n/2\log n + o(n/\log n)$ factors of size $\leq n^2$, when in fact the Erdos problem asks to factor into at most $n-n/\log n + o(n/\log n)$ factors of size $\leq n$, and at most $n/2-n/2\log n + o(n/\log n)$ factors of size $\leq n^2$. (The trivial factorization $n! = 1 \times \dots \times n$ would satisfy the previous versions of the theorems, which is what the AI-generated proof found.) So I am reopening PNT#648 PNT#649 to actually finish the proof of Erdos 392 (which is otherwise almost done outside of two small lemmas, including PNT#515 which is currently unclaimed).

Another cautionary tale not to blindly trust AI auto-formalization, even when it typechecks...

[Eric Vergo]

It sounds like you were able to catch this, in part, because the dependency graph is generated using the LeanArchitect system. Maybe checking for a disconnected dependency graph can be automated and happen as the dependency graph is being generated. It would be especially useful when working towards a specific result, such as this project.

[Thomas Zhu]

I'm happy our LeanArchitect tool helped in this case! Indeed, this level of dependency debugging is also one of its purposes.

[Eric Vergo]

Awesome, I made a feature request for this.

[Pietro Monticone]

Cool! Thanks @Terence Tao and @Eric Vergo.

[Terence Tao]

Happy to announce that the formalization of the solution to Erdos 392 is now complete. Many thanks to everyone who contributed to this solution, and particularly to @Alex Kontorovich for his heroic efforts in formalizing the final step (PNT#784) (which eluded two AI tools due to some non-trivial typos and refactoring required).