feat(OEIS): A087719

[rwst]

Resolves #1460.

Conjectures associated with A087719

Define $\varsigma(n)$ the smallest prime factor of $n$ (Nat.minFac). Let $a_n$ be the least
number such that the count of numbers $k \le a_n$ with $k > \varsigma(k)^n$ exceeds the count
of numbers with $k \le \varsigma(k)^n$.

The conjecture states that $a_n = 3^n + 3 \cdot 2^n + 6$ for $n \ge 1$.

References: oeis.org/A087719

Note: I'm using Claude + Opus for supervised formalization tasks. Claude has no permission to use git on my machine.

[mo271]

Suggested change

	rw [a, Nat.find_eq_iff]
	refine ⟨by decide, ?_⟩
	intro m hm
	interval_cases m <;> decide
	unfold a
	norm_num +decide only [Nat.find_eq_iff]

same for the other analogous proofs

[rwst]

I'm currently trying to steer Claude for a proof of the main theorem. I guess, if this succeeds then this PR is no longer of interest?

[rwst]

Okay, I have an ungolfed 500-line proof which eventually will be published as preprint on zenodo. What to do with this PR?

[mo271]

Fantastic, this is great! Let's keep the PR and merge it when ready, no problem that is not contains a research solved theorem instead of a research open conjecture. I propose to

• create an intermediary commit, adding the unfolfed 500-line proof
• delete that proof in the next commit and use our new formally solved tag to link to the commit with the ungolfed proof: feat(Util): add formally solved here option to the category tag #1851
• then update the docstring/references section once the preprint is out!

Nice to hear that writing up the proof formally lead to its solution, even before it was added to our repo!

[rwst]

I'm however not sure about the research label, exactly because this was proved by LLM. I'm not publishing because of its importance, but just to have a DOI to refer to.

[mo271]

There have been some examples recently of research problems, i.e. problems that were mentioned in a research paper, which have been solved with the help of AI.
If you think this is rather high school level or graduate or whatever, we can just use this label.
Perhaps we should expand our way to track formal proofs to all categories then. But as long as we don't have this it is also fine to provide the link to the proof in the docstring.
In any case, I think it is still nice to have this conjecture/theorem in our repo, thanks for making the effort formalising it.

Also: perhaps we can also add the mentioned generating function from this OEIS entry.

[rwst]

The g.f. simply reflects the formula. However, to add it would need some power series machinery, which I was planning to add for years already.

[mo271]

yeah, that makes sense. Perhaps the proof become easier using the g.f.
But it is also fine not to add it here.

I had thought everything is already in Mathlib, to at least state the power series identity? Using
PowerSeries.coeff ℤ or whatever. What machinery is missing?

[rwst]

I think it's more the combinatorial proofs that benefit from a g.f. What is missing are the lemmas to prove a power series of a rational function (like the g.f. here) have coefficients of form $\sum_i c_i*a_i^n$, with the $a_i$ the zeros of the function denominator.