Update on Consequences

Stream: PrimeNumberTheorem+

[(Tom de Groot) Tomodovodoo]

With the new PRs from me and Pietro, we have at least compiled every defined theorem at the moment; further issue is defining the (main) theorems surrounding the cyclotomic case. Two days ago this was enough, but it seems we are speeding through this faster than we thought. Is there anyone proficient to do this on a somewhat short basis?

For quick reference, here's the Github issue which further outlines the main goal for now in Consequences.

[(Tom de Groot) Tomodovodoo]

I've got all the free time in the world since I'm still on my (first) jobhunt after uni (seems after 4 months I am gonna be working a supermarket job soon to pay the bills :melting_face:), so I'd love to try to solve more, but I am not too confident in preparing/solving the first pieces of this puzzle in the definitions of theorems and sorries.

[(Tom de Groot) Tomodovodoo]

ah, it seems I missed Terrance's other chat from two days ago speaking about the exact same problem. Does anyone have some additional ideas on how to progress from this point?