(merged) #32776 grind and aesop annotations for ZMod

Stream: PR reviews

[Yoichi Hirai]

Hello, I'm trying to improve grind and aesop annotations for ZMod. This started in ItaLean 2025 workshop.

The first PR is in a good shape after some interactions with @euprunin (I don't know if they are on Zulip) and @Artie Khovanov . I am looking for a reviewer with write-access.

I'm a new contributor. Let me know if I'm doing something strange.

[Yoichi Hirai]

I was browsing the mathlib maintainer list. I can imagine explaining @Frédéric Dupuis my motivation for #32776 : better automation around ZMod will be useful for some cryptography.

[Yoichi Hirai]

I guess it's better to be transparent that the immediate purpose is to improve proofs in https://github.com/Verified-zkEVM/clean , though of course I suppose these annotations make everyone's life easier.

[Johan Commelin]

@Yoichi Hirai Thanks for the ping. We'll get to your PR. You can see the list of PRs that are waiting for review here: #queueboard
As you can see, there's quite a lot of PRs that are on this queue. The median time for a PR to get merged is ~ 6 days.

[Ruben Van de Velde]

(Don't ask about the average :sweat_smile:)

[Yoichi Hirai]

@Johan Commelin Thank you for the info! It's quite interesting to see the way things are organized here. I'm still calibrating my expectations.

[Johan Commelin]

On top of that, grind is still quite new, so many reviewers are still getting a feel for what are good grind annotations.

[Yoichi Hirai]

This one got merged. Thank you very much.