feat(Erdos/372): add largest prime factor chain statement

[bengoechea]

Summary

• Adds an Erdős Problem 372 statement file for the largest-prime-factor chain problem.
• Encodes Balog’s proved statement that there are infinitely many n such that P(n) > P(n+1) > P(n+2).
• Leaves the proof as sorry; no proof or external certificate is imported.

Source

• erdosproblems.com/372, accessed 2026-06-24. The page is marked PROVED and Formalised statement? No.

Validation

• lake build 'FormalConjectures.ErdosProblems.«372»'

Notes

• Statement-only formalization.
• Drafted with AI assistance and checked locally against the source page and targeted Lake build.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.