AKS primality test

Stream: PR reviews

[metakuntyyy]

So finally I learned lean good enough to tackle this nice number theoretical proof. I'm realistically about 60% through the proof, but it is quite gnarly and technical and there are quite a lot of decisions that I took pragmatically.

First PR is #34507 and that finishes Claim 1. It is about 10-20% of the estimated proof size.

Here are some questions. I designed this file to have one public declaration only which is the proof_wanted in the bottom of the PR. The rest are private declarations. I'm not sure if the introspective relation is worth having as a public declaration as it seems to be relevant for this proof only. Is this approach fine?

Here's the proof that I'm formalising https://academicweb.nd.edu/~andyp/notes/AKS.pdf It's theorem 6.1. Claim (i) is done in the PR. I don't know if it makes sense to share my local file. It is already 400 LoC and it's not cleaned up yet.

I'd like to have smaller managed PR's so that I don't overwhelm the review process.