tao

tao OP , 4 days ago

@Pashhur The blueprint does contain a lot of material (such as classical Calderon-Zygmund theory) that is quite standard in this area, and Thiele is one of the leading world experts in the subject and has not to my knowledge published anything with major errors in it. Furthermore, the blueprint is already rather more detailed than a traditional math paper, even if it has not yet been properly formalized. So I think there is a reasonable a priori probability to expect that the arguments are largely correct. That said, the formalization effort, despite being only a day or two old, has already uncovered some minor issues in the blueprint (a (k) should have been a (k+1) in one of the lemmas, for instance): https://leanprover.zulipchat.com/#narrow/stream/442935-Carleson/topic/Outstanding.20Tasks.2C.20V1

tao OP , 13 days ago (edited 13 days ago)

p.s., it may not have come across so well in the text transcription of the interview, but the portion about pressing a button to submit the GPT-generated LaTeX article to a journal was mostly made in jest. I would imagine journals in the future would develop filters, labeling requirements, and other rules regarding submissions that are partially or fully AI-generated, and that new cultural norms will emerge as to how to incorporate AI-generated texts as part of a scientific document (for instance, I could envision a framework in which it would be acceptable to link to an interactive AI-generated and Lean-integrated form of a paper as a secondary version, while retaining a human-written text as the primary authoritative version).

tao OP , 12 days ago

@alex I think adopting new workflow practices (such as those already standard in software engineering, or even in existing formalization projects) can address many of these issues. For instance, one should formalize the statement of the result before even starting the proof process, instead of afterwards. One could also semi-automatically or automatically subject the statement with various "sanity checks" or "unit tests", for instance testing trivial or very easy cases of the theorem, as well as known counterexamples to stronger versions of the theorem. (In my example, for instance, I included a verification of the converse to the theorem as a sort of sanity check, even though it was not actually needed for the goal.)

tao OP , 12 days ago

@cursv I am not aware of the literature in this area, though the Lean kernel is deliberately kept as small as possible (a few thousand lines of C++ code) and so it should be possible to perform formal verification in some external language.

While this is not the same thing, there is a tool to export a Lean proof to a file format that can be verified by independent software at https://www.scs.stanford.edu/16wi-cs240h/projects/selsam.pdf

Perhaps if you pose this question on https://proofassistants.stackexchange.com/ you might be able to get a more informed answer on this question.

tao OP , 14 days ago (edited 14 days ago)

Looking at this system, we see that only one of the conditions involves 𝑦, namely the constraint 𝑧=𝑥+𝑦², and this equation can be solved for 𝑦 if and only if 𝑧≥𝑥. So we can move 𝑦 "across the river" (this is an example of "quantifier elimination") and reduce to finding unknowns 𝑥,𝑧 solving the system 𝑥>0,𝑧≥𝑥 and 1/2<𝑧<√𝑥; a choice of variable 𝑦 can then be found in terms of these variables by either 𝑦=√(𝑧−𝑥) or 𝑦=−√(𝑧−𝑥) (one is free to choose either option).

Now looking at the new system, we see that the variable 𝑧 is the easiest to move "across the river": one can find a solution for 𝑧 in terms of 𝑥 as long as one has 𝑥,1/2≤√𝑥. Now we have a problem which only involves 𝑥, which is easy to solve by high school algebra, e.g., by setting 𝑥=1/2, thus moving the final variable 𝑥 "across the river" as well. Now we can unwind the process and find a candidate for 𝑧 (e.g., 𝑧=0.51 will work), and then a candidate for 𝑦 (in this case 𝑦=0.1 will work).

Of course, for solving nonlinear systems of equations involving real numbers, many other techniques (including fully automated computer algebra methods) are available, but I have found this sort of conceptual framework useful in the past for solving more compliciated types of problems, such as locating solutions to functional equations or partial differential equations, or more generally trying to prove a complicated existentially quantified assertion, in particular making the concept of "quantifier elimination" and "introduction of variables" visualizable as moving objects over the river and back across the river respectively. (2/2)

tao OP , 23 days ago

Guth and Maynard have managed to finally improve the Ingham bound, from 3/5=0.6 to 13/25=0.52. This propagates to many corresponding improvements in analytic number theory; for instance, the range for which we can prove a prime number theorem in almost all short intervals now improves from (\theta>1/6=0.166\dots) to (\theta>2/15=0.133\dots). (The Riemann hypothesis would imply that we can cover the full range (\theta>0)).

The arguments are largely Fourier analytic in nature. The first few steps are standard, and many analytic number theorists, including myself, who have attempted to break the Ingham bound, will recognize them; but they do a number of clever and unexpected maneuvers, including controlling a key matrix of phases (n^{it} = e^{it\log n}) by raising it to the sixth (!) power (which on the surface makes it significantly more complicated and intractable); refusing to simplify a certain complicated Fourier integral using stationary phase, and thus conceding a significant amount in the exponents, in order to retain a certain factorized form that ultimately turns out to be more useful than the stationary phase approximation; and dividing into cases depending on whether the locations where the large values of a Dirichlet series occur have small, medium, or large additive energy, and treating each case by a somewhat different argument. Here, the precise form of the phase function (t \log n) that is implicit in a Dirichlet series becomes incredibly important; this is an unexpected way to exploit the special features of the exponential sums arising from analytic number theory, as opposed to the more general exponential sums that one may encounter in harmonic analysis. (2/3)

tao OP , 23 days ago

As it turns out, both Larry and James will speak on this result later today at this conference: https://www.ias.edu/events/visions-arithmetic-and-beyond-celebrating-peter-sarnaks-work-and-impact-4 https://www.ias.edu/events/visions-arithmetic-and-beyond-celebrating-peter-sarnaks-work-and-impact-5 . (I unfortunately had to cancel participation in this event and will give a pre-recorded talk.) Larry and James are both excellent speakers and if you are interested in analytic number theory, I certainly recommend attending the talks. (3/3)

tao OP , 22 days ago

Talks are now available at https://www.ias.edu/video/new-bounds-large-values-dirichlet-polynomials-part-1 https://www.ias.edu/video/new-bounds-large-values-dirichlet-polynomials-part-2

The new progress can be summarized by the following chain of implications (see James' talk for some more detail):

Riemann Hypothesis
||
v
Lindelof Hypothesis
||
v
Density Hypothesis
||
v
Guth-Maynard zero-density estimate <- we are here
||
v
1940 Ingham zero density estimate
||
v
"Trivial" bound from Riemann-von Mangoldt formula

tao OP , 22 days ago (edited 22 days ago)

@highergeometer James addresses this at around 1:05:10 in the questions after his talk. Their work helps rule out the scenario of many somewhat bad violations of the Riemann Hypothesis (which is particularly helpful when trying to understand primes in short intervals), but doesn't make any new progress on ruling out one single extremely bad violation of the Riemann hypothesis, which is what zero-free regions are meant to exclude (and which play a central role in understanding primes in long intervals). The best zero-free region asymptotically is still the Vinogradov-Korobov zero-free region, which in this notation shows that 𝑁(σ,𝑇) is known to vanish completely once (\sigma \geq 1 - \log^{-2/3-o(1)} T). This result similarly has barely budged since 1958, and breaking that would similarly be a major advance in this field. (And in the q-aspect, eliminating Siegel zeroes would also be a major breakthrough on the zero free region front for L-functions.)

On the other hand, there are some useful improvements to zero density theorems (due to Turan, Halasz, and others) for σ near 1 that in some sense interpolate between the classical zero density theorems and the zero free regions, and in fact do better than the density conjecture for large values of σ.

tao OP , 22 days ago (edited 22 days ago)

@highergeometer Here is a quick effort (a few minutes with ChatGPT), plotting the best known exponents θ(σ) for which we have an estimate (N(\sigma,T) \ll T^{\theta(\sigma)+o(1)},) for various 1/2≤σ≤1. The lower the curves are, the better. The new improvement of Guth and Maynard improves upon the better of the Ingham and Huxley bounds near 3/4, but still does not reach the density conjecture in this range, although we have successfully established the density conjecture for somewhat larger values of σ. The known zero-free region roughly speaking corresponds to the bottom right corner of the image, and the Riemann hypothesis would push the entire diagram down to the x-axis. At the other extreme, the upper boundary θ=1 of this diagram corresponds to the trivial bound coming from the Riemann-von Mangoldt formula.

tao OP , 17 days ago

@Rowena I think a program to connect human grandparent volunteers to underresourced children could be very impactful, but to me the bottleneck for such a program would be the vetting of the volunteers, which is not something that technological aids are particularly equipped to resolve. So I would view such a program as quite complementary to an AI resource for such children, and in particular I don't see them being in any sort of conflict.

tao OP , 4 months ago

In many cases, what one wants to maximize is not the amount of criticism that one applies to an undesirable choice B (or amount of praise one applies to a desirable choice A), but rather the gradient of praise or criticism as a function of the desirability of the choice. For instance, rather than the maximizing magnitude of criticism directed at B, one wants to maximize the increase in criticism that is applied whenever the agent switches to a more undesirable choice B-, as well as the amount of criticism by which is reduced when the agent switches to a more desirable choice B+, where one takes into account all possible alternate choices B-, B+, etc., not just the ideal choice A that one ultimately wishes the agent to move towards. Thus, for instance, a company with a history of concealing all of its workplace accidents, who is considering a policy change to be more transparent about disclosing these accidents as a first step to working to resolve them, should actually be praised to some extent for taking this first step despite it causing more media coverage of its accidents, though of course the praise here should not be greater than the praise for actually reducing the accident rate, which in turn should not be greater than the praise for eliminating accidents altogether. Furthermore, one has to ensure that the direction of the gradient does not point in a direction that is orthogonal to, or even opposite to, the desired goal (e.g., pointing in the direction of preventing media coverage rather than improving workplace safety). (2/3)

tao OP , 4 months ago

In short, arguments of the form "B is undesirable; therefore we should increase punishment for B" and "A is desirable; therefore we should increase rewards for A", while simple, intuitive, and emotionally appealing, in fact rely on a logical fallacy that the the effect of incentives are monotone in the magnitude of the incentive (as opposed to the magnitude and direction of the gradient of incentive). I wonder if there is an existing name for this fallacy: the law of unintended consequences (or the concept of perverse incentives, or Goodhart's law) are certainly related to this fallacy (in that they explain why it is a fallacy), but it would be good to have a standard way of referring to the fallacy itself.

In any case, I think political discourse contains too much discussion of magnitudes of incentives, and nowhere near enough discussion of gradients of incentives. Which raises the meta-question: what incentive structures could one offer to change this situation?
(3/3)