Bombieri–Lang conjecture

### What is the conjecture
Higher dimensional version of Faltings Theorem.

See more here:
https://en.wikipedia.org/wiki/Bombieri%E2%80%93Lang_conjecture

### Prerequisites needed
Missing a lot of infrastructure in mathlib.

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Read the Bombieri–Lang conjecture description and the linked Wikipedia article first, then assess the missing mathlib infrastructure mentioned in the issue. Done means adding a formalized statement of the conjecture to the repository, but the issue does not identify files, entry points, or tests.

Written by the indexing model from the issue text.