Diophantine approximation (or: a formalization surprise)

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Hi all,

Just wanted to report another success for Aristotle.

Last night, I asked it to formalize the first two lemmas in Part I of my ternary Goldbach book draft. The first lemma is just Dirichlet's Diophantine approximation theorem, with $Q$ real; mathlib already has a very close variant. The second lemma is the more interesting one, in that it is not in mathlib, or elsewhere in the literature: it states that, given a Diophantine approximation to a real $\alpha$ with error $\epsilon$, you can find another valid approximation $a'/q'$ such that $q'$ lies in a prescribed dyadic range depending on $\epsilon$.

[Harald Helfgott]

I tried two approaches:

1. I gave Aristotle essentially the LaTeX for the section essentially verbatim (just removing commentary and citations). This is
   diophapprox.txt. I'm also including a version
   diophapprox.tex with commentary and citations edited back in, and formatted so that they do not depend on a bibliography file. This was really something I was doing late at night, almost for a lark.

2. Then I rewrote the txt file so as to make it something closer to a blueprint, indicating to Aristotle that there was something equivalent to the first lemma in Mathlib, and also breaking down the second lemma into several lemmatia. This is
   diophapprox_purple2.txt.

Guess what: Aristotle proved both versions within about an hour.

Here are the generated .lean files:
diophapprox-output.lean
diophapprox_purple2-output.lean
They type-check, and, as far as I can tell, the statements do correspond to what was asked; I'd be very happy if others could double-check.

If this holds up, I think the second lemma (Lemma 2.2 in the book draft) would be a good candidate to add to the blueprint tree (or forest).

[Terence Tao]

Just for the record, if one wants to add a new Lean file (containing blueprint tags) to the project as a PR, one has to do the following

1. Make sure Architect is imported, either directly or indirectly, in the Lean file
2. Add the Lean file as an import to the top-level lean file PrimeNumberTheoremAnd.lean
3. Also add the Lean file as an \inputleanmodule{} somewhere in blueprint.tex
4. Format the Lean and LaTeX using the blueprint_comment and @blueprint[] functions (one can look at other Lean files in the repository for examples.
5. If there are references, update references.bib in the blueprint directory accordingly.
6. If new LaTeX macros are introduced, update the initial part of `blueprint.tex' accordingly.

(I'll go ahead and add these notes to CONTRIBUTING.md.)

[Pietro Monticone]

Yes, precisely.

[Harald Helfgott]

Thanks, Terry. What does adding the notes to CONTRIBUTING.md do? Does it incorporate them to the blueprint tree?

[Terence Tao]

No; CONTRIBUTING.md is our guide to contributors for how to make contributions to the Github repository (this is a standard component of many open source projects run on Github).

[Harald Helfgott]

Ah, OK. So, if I follow these instructions, the blueprint will be incorporated to the blueprint tree? Surely one should specify where it is to be added?

[Terence Tao]

You can choose where in blueprint.tex you will import the Lean file; this will determine the placement of the file in the current blueprint tree. I'll update the instructions in CONTRIBUTING.md to reflect this.