google-deepmind / google-deepmind/formal-conjectures
Green's Open Problems #99
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 2d 4h
- Merged PRs (30d)
- 363
Description
### What is the conjecture
https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.99
As #1754 illustrates, finding a single solution to a polynomial equation $F(x\_1, ..., x\_n) = C$ (say) can be very difficult, and asymptotically enumerating such solutions inside (say) a box $[X]^n$ is still harder. Nonetheless, one may ask about going yet further, and pose the question of estimating the number of solutions with the $x\_i$ constrained to lie in some set $A \subset [X]$. In particular, what conditions on $A$ ensure that the number of such solutions is roughly $\alpha^n$ times the number of solutions in $[X]$, where $\alpha := |A|/X$ is the density of $A$ in $[X]$, imagining here that $\alpha \in (0,1)$ is fixed and $X$ is large?
When $F$ is linear (and $n \geq 3$) such a condition is that $A$ has no large Fourier coefficients, that is to say $X^{-1} |\sum\_{x \leq X} (1\_A(x) - \alpha)e(\theta x)| = o(1)$ uniformly in $\theta$. Some questions are
(i) What can be said when $\deg F = 2$ and $n = 7$, at least in the 'generic' case?
(ii) What is the least value of $n$ for which one can say something in the case $\deg F = 3$, at least in the 'generic' case?
(iii) What about specific interesting cases such as $F(x\_1, x\_2, x\_3, x\_4) = x\_1^2 + x\_2^2 + x\_3^2 + x\_4^2$?
### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)
* ams-11
* ams-05
### 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
Contributor guide
Research direction
Read Green's linked open-problems paper at problem 99 and review existing formalized conjectures in the repository for the expected statement style. The work is done when this conjecture is added to the Lean collection with its relevant AMS categories and a faithful formal statement.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 25/100