I'm looking for some readable proofs to get a hang of Coq with (both with and without SSReflect). Ideally, mathematically interesting statements, more than just the type of ab=ba. But not too deep or complicated; in particular I prefer to avoid long semicolon chains. Any suggestions?

Other than the book you probably remember, there is some teaching material here: https://math-comp.github.io/

yeah I remember that book :) but I was hoping for something more hands-on, something like a particularly low-tech proof of e.g. quadratic reciprocity with comments explaining the tactics and notations used as they arise

the book is on my mental desk already

hmm this looks like a good start https://github.com/coq-community/coq-100-theorems/blob/master/ballot.v

I would also be interested in such suggestions, and I was asking a similar question here yesterday while working on the Getting Started wiki page. @Darij Grinberg did you find some examples that were helpful?

trying out ballot.v for now, will let you know if I finish it without much confusion

Maybe too 'deep', but I find https://madiot.fr/coq100/ to be a reasonable way to find real math problems solved in Coq.

Last updated: Sep 30 2023 at 06:01 UTC