The final release of Coq 8.4 is now available. Its features among other things a modular and uniform extension of the arithmetical libraries and a new proof engine providing bullets. See the dedicated page or download page for more details.
Recent news
The Coq team has decided that Coq will be renamed into 'The Rocq Prover'. Background information available here. The rename is currently in preparation, we hope to have a new visual identity and website by early 2025, and to do a first release of Rocq around that time.
There is now a Stack Exchange Q&A site dedicated to Proof Assistants! Do not hesitate to post and answer Coq questions there (use the coq tag).