feat(ErdosProblems): 82#1395

Merged

mo271 merged 5 commits intogoogle-deepmind:mainfrom

Mal-Pat:erdos-82

Jan 17, 2026

Commits on Dec 5, 2025

Formalized the statement of Erdos Problem 82
Mal-Pat
committed

Commits on Dec 15, 2025

Commits on Dec 16, 2025

Improve formatting and formalization of `F n`
Mal-Pat
committed

Commits on Dec 18, 2025

Fix type of `3 / 4` to `ℝ`
Mal-Pat
committed