Values of higher least non-divisors

[David Radcliffe]

Hello fellow humans,

Sequence A007978 lists the least non-divisor of n. The first 10 terms, starting at n=1, are 2, 3, 2, 3, 2, 4, 2, 3, 2, 3. 

It is not hard to prove that every term in this sequence is a prime power, and that every prime power appears in the sequence.

Sequence A396771 lists the second least non-divisor of n. The first 10 terms, starting at n=1, are 3, 4, 4, 5, 3, 5, 3, 5, 4, 4. 

One can show m is a value of this sequence if and only if m ≥ 3 and m is either a prime power or twice a prime power.

One can consider higher non-divisors. The OEIS has no entry for the third least non-divisor of n. 

Nevertheless, it is not too difficult to prove that m is the third least non-divisor of some integer n if and only if 

m ≥ 4 and m = a * p^s where a is in {1, 2, 3}, p is prime, and s ≥ 1.

This suggests a natural conjecture. Let e_r (n) be the r-th least positive integer that does not divide n.

Then m occurs as a value of e_r if and only if m ≥ r + 1 and m = a * p^s where p is prime, s ≥ 1, and 1 ≤ a ≤ r.

One direction is routine. Suppose that e_r(n) = m. It is clear that m ≥ r + 1, since 1 is a divisor of n. Since m does not divide n, 

there exists a prime p so that s := ν_p(m) > v_p(n), where v_p(n) denotes the exponent of p in the prime factorization of n. 

Let a = m / p^s.  Then p^s, 2 * p^s, ..., a * p^s are non-divisors of n, and a * p^s = m, hence 1 ≤ a ≤ r.

I have a supposed proof of the other direction, generated using AI tools. The proof is only seven pages long, 

but I hesitate to share it since it is difficult to read and there is a surfeit of AI-generated math papers. 

Can anyone propose a more human proof?

Thanks,

David

[Allan Wechsler]

A bit off-topic: something that people can do to become more confident of AI-authored proofs is to ask the AI to present the proof in Lean 4.

Then, you can often inspect the Lean statement of the theorem, and at least confirm to your satisfaction that it is trying to prove the claim you actually have in mind (instead of some other weird claim); and then if you feel up to it, you can actually try to compile the proof in Lean to see if the Lean compiler considers the proof to be valid.

(I recently learned that the way Lean says, "Hey, this proof is invalid!" is by emitting compiler errors. The way it says a proof is okay is by saying nothing. That is, you type lean myproof.lean into your shell, and it just responds (after a pause) with the shell prompt. This seemed strangely anticlimactic to me, but that's the way it is.)

This, of course, doesn't address the humanistic problem of AI-authored mathematics, but at least it can dispel the suspicion that the AI is just lying.

This is also how we should be talking to those who still think Mochizuki proved the abc conjecture. Ask for a formalization in Lean 4. This has been done for the four-color map theorem, the Poincare Conjecture, and Fermat's Last Theorem. It hasn't been done for the existence of the Fischer-Griess Monster Group: this is apparently a big technical challenge due to the structure of the argument.

-- Allan

--
You received this message because you are subscribed to the Google Groups "SeqFan" group.
To unsubscribe from this group and stop receiving emails from it, send an email to seqfan+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/seqfan/CAJ7c8C%3D3o0O3nOU%2BdzeBhKTpEdYjC0pB4nyOgqA2AqvNYWRQjQ%40mail.gmail.com.

[Tomasz Ordowski]

It would be best to get Chinese PhD students interested in this.

To view this discussion visit https://groups.google.com/d/msgid/seqfan/CADy-sGEJsUm%2BUEp9sOw6ti-PHzd%3DaPqf%3DVZ%2BjbXgc%3D670mDrQg%40mail.gmail.com.