google-deepmind / google-deepmind/formal-conjectures

Green's Open Problems #99

Open
#1,755 0 comments 0 reactions 0 assignees View on GitHub
green-problems new conjecture
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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.