[Paul-Lez]

Summary

• add Challenge.lean and Solution.lean for the ζ(5) irrationality benchmark
• cite the pinned Formal Conjectures statement and include its copyright header
• add Comparator CI configuration and formalization.yaml
• keep the README concise while documenting Formal Conjectures, dependencies, and proof sources

Validation

• lake env lean Challenge.lean
• metadata parsing and schema validation
• git diff --check

[mo271]

I took those commits to #2