I’m learning to use Rocq, I felt very powerful.

The amount of times I’ve been unsure of how to word something so I just write “it’s clear that…”
”The proof is trivial and is left as an exercise for the reader”
Submitting this as my paper on the Riemann Hypothesis
The reader can clearly see…
“Trivial” and “naive”.
And I’m looking at Nima Arkani Hamed, he’s either a physicist or cosmologist or both, but in every lecture or interview, if he doesn’t use either word “trivial” or “naive” every minute or so, his forehead veins start popping out and he starts sweating. He can’t be bothered to explain what is evidently obvious… to him, in his ivory tower, so he takes constant fucking non-explanation shortcuts.I’m learning to use Rocq
Willingly? Damnnnnnn
Somewhat, I’m quite motivated but it’s part of my studies.
What is Rocq? Some sort of formal proof writer/checker?
Yes exactly that. It was previously called Coq, maybe you know it under that name?



