Formalizing a conjecture in explicit Class Field Theory

Stream: maths

[David Bernier]

I've been asking the AI Aristotle to try to prove a result in what might be called explicit Class Field Theory.
The general statement is as follows:

Let q be a prime such that a^2 = 4q-27 for some positive integer a. Let N be an odd prime such that N=/=q and gcd(a,N)=1. Let s1 == (-a-3)/6 (mod q) and s2 == (a-3)/6 (mod q). Let f=x^3-qx-q. Assume that f is irreducible modulo N. Let c == N^((q-1)/3) (mod q). Let K be a splitting field of f over F_N. Let alpha be a root of f in K. Let beta in K be such that
2a beta = 6 alpha^2 - (a+9)alpha - 4q and gamma in K be such that alpha + beta + gamma = 0.
Then, alpha^N = gamma if c == s1 (mod q) and
alpha^N = beta if c == s2 (mod q).

This problem was the subject of a question of mine at Mathematics Stack Exchange: https://math.stackexchange.com/questions/5075981/how-to-determine-which-of-two-conjugate-roots-is-the-frobenius-of-alpha. So far, there have been no answers.

Aristotle was successful in proving the q=7 case of this (conjectural) result. I often submit to Aristotle TeX files containing sketches of proofs, drawn up by AIs.

Here is Aristotle's proof for q=7 in outline:

We can view the splitting field of X^3 -7X -7 as a subfield of the cyclotomic field Q(zeta_7​) because the roots of the polynomial can be explicitly constructed from Gaussian periods of Q(zeta_7). The three real roots satisfy algebraic relations like
4b956492-22b0-4b56-9fb4-b4478653c500-output_fixed5.lean
beta = 3 alpha^2 - 5 alpha - 14 and gamma = -3 alpha^2 + 4 alpha + 14. The proof studies the automorphism sigma_N of Q(zeta_7) obtained from the relation sigma_N(zeta_7) = (zeta_7)^N. It shows that if N == +/- 3 (mod 7), then sigma_N(alpha) = beta, while if N == +/- 2 (mod 7), then sigma_N(alpha) = gamma. It proves the Artin symbol property, i.e. sigma_N reduces to the Frobenius map x |-> x^N (mod P) where
P is a prime ideal over N. Finally, the proof gives two theorems concerning explicit Frobenius action on alpha.

​I'd be interested in learning of tips or ideas on how to get Aristotle to autoformalize the conjectural result for general q.

I'm taking the liberty of attaching Aristotle's Lean proof for the case q=7.

[Kevin Buzzard]

Does this question say "I'd be interested in learning of tips or ideas on how to get Aristotle to prove a theorem that nobody knows how to prove?" because if it does then I have the same question for the Riemann Hypothesis. Or do I misunderstand you?

I am not sure I have the energy to unravel this question but doesn't cubic reciprocity (see eg Ireland-Rosen) give you a way of unraveling which cube root of unity you get? Or isn't this enough?

[Antoine Chambert-Loir]

And one should not confuse “nobody took the time to answer a question on StackExchange” with “nobody knows how to prove it”.

[Kevin Buzzard]

Fair enough, it certainly looks accessible, but I'm not sure that Aristotle will know enough about cubic reciprocity (which is not in mathlib) so I don't think it has a chance really (I would love to be proven wrong).

[Yury G. Kudryashov]

I think I won't disclose any commercial secrets if I say that this task (adding a theory that isn't in Mathlib, then solving a problem on top of it) is too difficult for the time/resources budget we allow on a single public API call. One can build a theory in a sequence of API calls, with the next one providing the previous output with context and new hints, then ask Aristotle to solve the problem.

[Filippo A. E. Nuccio]

Just out of curiousity, did you explicitly tell Aristotle to focus on the q=7 case ot it did it autonomously?

[David Bernier]

Yes, I explicitly told Aristotle to focus on the q=7 case. Also, all the terms involving q or a=sqrt(4q-27) were evaluated. One reason I am mildly optimistic that it's accessible is that A.O.L. Atkin developed and implemented a cubic primality test in the '90s. His cubic test predicts x^N (mod f, N), where f is a cubic polynomial in x with parameter a prime q=1 (mod 3), and where N is a prime such that N^((q-1)/3) (mod q) is neither 0 nor 1.
The details (without proof) are in: A.O.L. Atkin, "Intelligent Primality Test Offer", Proceedings of a Conference in Honor of A.O.L. Atkin, 1998.

[Filippo A. E. Nuccio]

Thanks, I'll have a look at the details as soon as I get more time :sweat_smile:

[David Bernier]

It seems my original formalization goal was a bit too ambitious. Aristotle has found proofs for about 12 special cases: q = 7, 13, 19, 37, 79, 97, ... 709 (the value of the prime N isn't restricted). These proofs all use the cyclotomic field Q(zeta_q) to express the roots of X^3 - qX - q over Q as differences of Gaussian periods of degree 3. Then, the splitting field of X^3 - qX - q over Q may be viewed as a subfield of Q(zeta_q).

I'm not a number theorist, so I don't know whether cubic reciprocity is enough to answer the question. I have kept copies of the Lean proofs, and they all compile without errors and have no sorries, but aren't polished. I'd be grateful if someone from the community could have a quick look at one of the Lean proofs, e.g. to check that the question wasn't misformalized.

[Antoine Chambert-Loir]

I'm puzzled. Why would you ever be interested in formalizing a possibly open question in explicit class field theory if you're not interested in understanding the proof by yourself?

[David Bernier]

I'm interested in this class field theory question for its potential application to probabilistic primality testing: if a number fails the test, then it is definitely composite (assuming the conjecture in class field theory). I realize that the Baillie-PSW probabilistic primality test is extraordinarily discriminating, but nevertheless am still curious about probabilistic primality tests involving cubic polynomials.

I am somewhat interested in understanding the proofs, as long as they are in natural language. A proof in Lean gives me high assurance that the result is correct, although I remain concerned about misformalizations. In what follows, I work out two examples applying the conjectural proposition, and mark its use by an asterisk (*).

Let the test number N be 5771. One finds that for q = 163, a = sqrt(4*163-27) = 25, and N^((q-1)/3) == 58 (mod 163). One has s1 = (-a-3)/6 = (-25-3)/6 (mod 163), or s1=104 (mod 163) and s2 = (a-3)/6 = 58 (mod 163), so if N is prime, alpha^N is predicted (*) to be: (6 alpha^2 - (a+9)alpha - 4q)/(2a) = 1616 alpha^2 + 461 alpha + 1372. Using Pari/gp, I find that alpha^N = 4087 alpha^2 + 3060 alpha + 5178 (not matching the prediction). If I know the conjecture is true for q=163, then I can state with confidence that N is composite. (5771 = 29*199)

Sanity check: Let N = nextprime(5771) = 5779. N^((q-1)/3) = 104 = s1, so the prediction (*) is alpha^N = gamma. One computes that beta = 4161 alpha^2 + 5316 alpha + 4379 and gamma = -(alpha+beta) = 1618 alpha^2 + 462 alpha + 1400 (the prediction), while alpha^N = 1618 alpha^2 + 462 alpha + 1400 (a match with the prediction). Therefore, the test reports 5779 as probably prime, which it is.

P.S. In the first example, I should have said that the computation of alpha^N is done in the ring (Z/NZ)[x]/(x^3-163x-163) and that alpha is defined by alpha = x (mod N, x^3-163x-163). I apologize for the omission.

[Franz Huschenbeth]

David Bernier said:

It seems my original formalization goal was a bit too ambitious. Aristotle has found proofs for about 12 special cases: q = 7, 13, 19, 37, 79, 97, ... 709 (the value of the prime N isn't restricted). These proofs all use the cyclotomic field Q(zeta_q) to express the roots of X^3 - qX - q over Q as differences of Gaussian periods of degree 3. Then, the splitting field of X^3 - qX - q over Q may be viewed as a subfield of Q(zeta_q).

I'm not a number theorist, so I don't know whether cubic reciprocity is enough to answer the question. I have kept copies of the Lean proofs, and they all compile without errors and have no sorries, but aren't polished. I'd be grateful if someone from the community could have a quick look at one of the Lean proofs, e.g. to check that the question wasn't misformalized.

You mean to check the formalized statement, we dont need to check the proof the kernel does that. I think it would make sense, that you learn to read formalized statements in Lean yourself, the best resource for that is probably https://github.com/leanprover-community/mathematics_in_lean.

[Filippo A. E. Nuccio]

David Bernier said:

It seems my original formalization goal was a bit too ambitious. Aristotle has found proofs for about 12 special cases: q = 7, 13, 19, 37, 79, 97, ... 709 (the value of the prime N isn't restricted). These proofs all use the cyclotomic field Q(zeta_q) to express the roots of X^3 - qX - q over Q as differences of Gaussian periods of degree 3. Then, the splitting field of X^3 - qX - q over Q may be viewed as a subfield of Q(zeta_q).

I'm not a number theorist, so I don't know whether cubic reciprocity is enough to answer the question. I have kept copies of the Lean proofs, and they all compile without errors and have no sorries, but aren't polished. I'd be grateful if someone from the community could have a quick look at one of the Lean proofs, e.g. to check that the question wasn't misformalized.

Are these files in a GitHub repo or just on your laptop?

[Antoine Chambert-Loir]

David Bernier said:

I don't know whether cubic reciprocity is enough to answer the question.

To bring some hopefully constructive remark to the discussion: Kevin, myself, Filippo, and many others here are number theorists, and as our reactions suggest, we believe that cubic reciprocity should do the job. But this is a belief, an intuition, I'd guess that none of us did the actual work of writing down the arguments. Your cryptographic motivation is definitely legitimate, but at this point, I believe it is your job to try to put cubic reciprocity into the machine and see what it says about your question. Likely, you will first struggle to understand some statements, and to apply them effectively, but I guess that you will be able to find help here. In the end, if that works, you will have learnt something, and so will we; and if that doesn't work, you will also have learnt something, and certainly made some move towards the next step to the solution of your problem. This is how mathematical research works.

[David Bernier]

Filippo A. E. Nuccio said:

David Bernier said:

It seems my original formalization goal was a bit too ambitious. Aristotle has found proofs for about 12 special cases: q = 7, 13, 19, 37, 79, 97, ... 709 (the value of the prime N isn't restricted). These proofs all use the cyclotomic field Q(zeta_q) to express the roots of X^3 - qX - q over Q as differences of Gaussian periods of degree 3. Then, the splitting field of X^3 - qX - q over Q may be viewed as a subfield of Q(zeta_q).

I'm not a number theorist, so I don't know whether cubic reciprocity is enough to answer the question. I have kept copies of the Lean proofs, and they all compile without errors and have no sorries, but aren't polished. I'd be grateful if someone from the community could have a quick look at one of the Lean proofs, e.g. to check that the question wasn't misformalized.

Are these files in a GitHub repo or just on your laptop?

I've uploaded 13 Lean files by Aristotle to the following Github repo: https://github.com/mariotrevi/cubic-frobenius-lean. Besides the cases q = 7, 13, 19, 37, ... 709, there is also a file for q=877 that compiles without errors.

[Kim Morrison]

@David Bernier, a git repository containing lean files but without a lean-toolchain or lakefile.toml is essentially worthless. (In fact, it's one of the basic filters we use for "is this AI slop that is a waste of everyone's time". I can see from the discussion above that you don't intend or want to waste everyone's time: this is intended as a helpful suggestion as to how you can make effective use of peoples' willingness to help you!)

[David Bernier]

Kim Morrison said:

David Bernier, a git repository containing lean files but without a lean-toolchain or lakefile.toml is essentially worthless. (In fact, it's one of the basic filters we use for "is this AI slop that is a waste of everyone's time". I can see from the discussion above that you don't intend or want to waste everyone's time: this is intended as a helpful suggestion as to how you can make effective use of peoples' willingness to help you!)

Thank you for telling me about this. I've updated my repo by adding a lean-toolchain file and a lakefile.lean file. I've tested the updated repo by cloning it to my local machine. I then ran lake update and lake exe cache get . Then I compiled succesfully two of the Lean files using lake env lean filename.