feat(Erdos/175): add central binomial squarefree statement

[bengoechea]

Summary

• Adds an Erdős Problem 175 statement file for the central binomial coefficient squarefreeness problem.
• Encodes the proved statement that for every n ≥ 5, Nat.choose (2 * n) n is not squarefree.
• Leaves the proof as sorry; no proof or external certificate is imported.

Source

• erdosproblems.com/175, accessed 2026-06-24.

Validation

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

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.