Aristotle as solver for mu_pnt and mu_pnt_alt

Stream: PrimeNumberTheorem+

[(Tom de Groot) Tomodovodoo]

Heya,

I wanted to see if I can use Aristotle to solve some of PNT, at least some open already defined equations.

At the moment, I focused on Consequences.lean, but I find it quite an ugly solve, requiring many exact? tactics and the like (simpa's which are not needed, etc etc). I've tried for some time to manually find better representations for many parts, but to be honest, with being new to lean and my mediocre mathematics compared to many here, I am struggling.

Additionally, Aristotle requires an environment of 4.24, so porting and backporting some theorems from 4.26 was quite a challenge. I finally have both environments setup, (not how well as I'd want to, but oh well)

My question:

1. I have mu_pnt and mu_pnt_alt now fully defined, without errors compiling in lean 4.24; Can I port this over with relative ease to lean 4.26? Additionally, would the backbone lemmas for the port also require blueprints?
2. The current solves are done with quite a few exact? tactics, and two of the lemmas also required an additional maxHeartbeats to compile without errors. Would this be an issue when creating a PR?
3. Is this even useful, or is this project solely based on fully human derived .lean code? I'd understand if what I'm writing is complete slop that just compiles, that that is not what is desired.

Hope I'm not intruding too much...

[Ruben Van de Velde]

At least any exact? calls need to be replaced by their output

[Ruben Van de Velde]

As for going back and forth between 4.24 and 4.26, I forsee no fundamental issues, but perhaps some tedious adjustments. You can check my bump pull requests to see what kinds of changes are needed

[(Tom de Groot) Tomodovodoo]

Update, worked through the refine' and exact? tactics so they're worked out at least; just 2 of them now depend on the (in the .lean file defined) GeneralizeProofs (Harmonic.GeneralizeProofs). Is it a requirement or good practise to refine the proofs to not rely on this?

[(Tom de Groot) Tomodovodoo]

Ruben Van de Velde said:

At least any exact? calls need to be replaced by their output

yeah, got so far luckily :P

[Ruben Van de Velde]

Is that something else than the generalize_proofs tactic from mathlib?

[(Tom de Groot) Tomodovodoo]

I believe Aristotle uses a slightly modified version of generalize_proofs from mathlib, and to ensure correct compilation, they include it in the output .lean file when needed. Additionally, they're still on 4.24 so I've just been busy with fixing mismatches between them

[(Tom de Groot) Tomodovodoo]

For example I have to rewire some stuff since in mathlib the ArithmaticFuntion library changed quite a bit, and that's the current struggle

[(Tom de Groot) Tomodovodoo]

Got at least the 4.24 version fully running without any warnings; Port to 4.26 is more than tedious, I got it compiled but a PR will take some time...

[(Tom de Groot) Tomodovodoo]

is a higher set maxHeartbeats allowed for PNTA? Currently, I have two lemmas which rely on a simp which doesn't resolve in the base amount of 200000. (set to 800000 for now)

[(Tom de Groot) Tomodovodoo]

added PR here for review; unsure about the feedback on this one, so please give as much as possible :P.

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/456

[(Tom de Groot) Tomodovodoo]

Refactored as best to my ability to cut down on unallowed tactics for PNTA like exact? and refine', couldn't improve on the max heartbeats myself, but im sure this is suboptimal and can be (heavily) improved

[Ruben Van de Velde]

There's already a few files that are very painfully slow, I wouldn't look forward to having more of them. But it's not my call to make

[Terence Tao]

I'm expecting the formalization of the explicit prime number theorem estimates to be heavily AI assisted and likely full of slow, heartbeat-intensive proofs. But this doesn't mean that we should abandon any effort at possible efficiency improvements. One possible compromise is to accept these proofs for now but add a task later to "golf" the proof to make it faster. (One could imagine that this latter golfing is also something that AI tools might be good at...)

[Alastair Irving]

Its not my call but personally I wouldn't be in favour of adding so much untidy AI generated code to the repo. If we were going to do that then we could have just taken the existing AI proof of strong PNT. The issue with these AI proofs is that they often seem to miss existing Mathlib API and reprove things from first principals. I only looked at the start of the PR but it feels like many of the manipulations of sums of arithmetic functions could be done much more cleanly.

At a minimum I think we should require all the warnings from the linters to be fixed before this is merged.

[Harald Helfgott]

Even in the non-formal regime, "golfing" (golfing little lemmas, that is; it's pointless to ask AI to do much more at this stage) is something at which AI is worse than a competent human mathematician, but the two working together can do a faster and arguably better job than the mathematician working alone.

[(Tom de Groot) Tomodovodoo]

Ah sorry, it seems during the build compared to my simple lake env lean command there are additional linter warnings that locally did not show up for me, I'll do my best to fix those of course. I only had the linter warning for "warning: unused variable x" remaining, but the build revealed much more.

Of course, I'll fix all the additional linter warnings, also I have one question;

For the function mu_pnt_alt, currently it is defined as follows:
theorem mu_pnt_alt : (fun x : ℝ ↦ ∑ n ∈ range ⌊x⌋₊, (μ n : ℝ) / n) =o[atTop] fun x ↦ (1 : ℝ) := by
however, the linter also recognizes that x is unused here; .\PrimeNumberTheoremAnd\Consequences.lean:2503:81: warning: unused variable x
I kept the definition like this for now since i figured it wouldn't do any harm, does anyone have some better insights as to keep or remove the variable?

Additionally, unlike many of the great mathematicians here, I am not properly proficient in lean yet (or as in-depth in the mathematics as you are). I'll try to reduce the amount of unnecessary code as much as I'm able, since it seems the current PR is not up to standard yet.

[Ruben Van de Velde]

You can write fun _ instead

[(Tom de Groot) Tomodovodoo]

Yeah I know, just didn't want to mess with the definition, if it aint broken dont fix it was my idea