The proof is not too bad in Lean4. I'm nothing special and I've got it down to 9 lines. But, maybe that is considered pretty tedious vs. what expectations one might have. In any case, it is an exercise in Heather MacBeth's free book: The Mechanics of Proof,

https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur...

btw, that book is a lot of fun to work through.

The obvious proof term for isprime p is exponential compared to the size of p. The AKS proof term is polynomial, but still very bad.

Is it? You can tell the checker about the remainder of division by 2 to 6.

Maybe also need to show that there are no other naturals between 1 and 7? And also that numbers greater than 7 can't be a divisor of 7?

The first one can be trivially proved with automatic decision procedures and the second one is also very easy to prove, I believe.