# \#mathcomp

**URL:** https://discourse.rocq-prover.org/tag/mathcomp/4.md

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

---

## [Seventeenth Mathcomp sharing day](https://discourse.rocq-prover.org/t/seventeenth-mathcomp-sharing-day/3069)

<div class="topic-metadata">

**Author:** [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Replies:** 0\
**Last updated:** [July 8, 2026, 2:24pm UTC](https://discourse.rocq-prover.org/t/seventeenth-mathcomp-sharing-day/3069 "2026-07-08T14:24:53Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our 17th “Mathcomp sharing day”. On July 15th, 2026, from 1am UTC (3am Paris time or 10am Tokyo time), to 3pm UTC (5pm Paris time or m…

---

## [Sixteenth Mathcomp sharing day](https://discourse.rocq-prover.org/t/sixteenth-mathcomp-sharing-day/3031)

<div class="topic-metadata">

**Author:** [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Replies:** 0\
**Last updated:** [May 18, 2026, 3:12pm UTC](https://discourse.rocq-prover.org/t/sixteenth-mathcomp-sharing-day/3031 "2026-05-18T15:12:22Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our 16th “Mathcomp sharing day”. On May 27th, 2026, from 1am UTC (3am Paris time or 10am Tokyo time), to 3pm UTC (5pm Paris time or mi…

---

## [Fifteenth Mathcomp sharing day](https://discourse.rocq-prover.org/t/fifteenth-mathcomp-sharing-day/2944)

<div class="topic-metadata">

**Author:** [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Replies:** 0\
**Last updated:** [February 23, 2026, 2:13pm UTC](https://discourse.rocq-prover.org/t/fifteenth-mathcomp-sharing-day/2944 "2026-02-23T14:13:51Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our fifteenth “Mathcomp sharing day”. On February 25th 2026, from 10am to 5pm Paris time, MathComp users, from enthusiasts to experts, a…

---

## [Fourteenth Mathcomp sharing days](https://discourse.rocq-prover.org/t/fourteenth-mathcomp-sharing-days/2912)

<div class="topic-metadata">

**Author:** [@CohenCyril](https://discourse.rocq-prover.org/u/CohenCyril)\
**Replies:** 0\
**Last updated:** [January 23, 2026, 1:22pm UTC](https://discourse.rocq-prover.org/t/fourteenth-mathcomp-sharing-days/2912 "2026-01-23T13:22:26Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our fourteenth “Mathcomp sharing day”. On January 28th 2026, from 10am to 5pm Paris time, MathComp users, from enthusiasts to experts, a…

---

## [Thirteenth Mathcomp sharing day](https://discourse.rocq-prover.org/t/thirteenth-mathcomp-sharing-day/2850)

<div class="topic-metadata">

**Author:** [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Replies:** 0\
**Last updated:** [November 24, 2025, 1:08pm UTC](https://discourse.rocq-prover.org/t/thirteenth-mathcomp-sharing-day/2850 "2025-11-24T13:08:01Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our thirteenth “Mathcomp sharing day”. On November 26th 2025, from 10am to 5pm Paris time, MathComp users, from enthusiasts to experts, …

---

## [Twelfth Mathcomp sharing day](https://discourse.rocq-prover.org/t/twelfth-mathcomp-sharing-day/2830)

<div class="topic-metadata">

**Author:** [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Replies:** 0\
**Last updated:** [September 18, 2025, 1:10pm UTC](https://discourse.rocq-prover.org/t/twelfth-mathcomp-sharing-day/2830 "2025-09-18T13:10:37Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our twelfth “Mathcomp sharing day”. On September 24th 2025, from 10am to 5pm Paris time, mathcomp users, from enthusiasts to experts, ar…

---

## [MathComp 2.4.0 released](https://discourse.rocq-prover.org/t/mathcomp-2-4-0-released/2632)

<div class="topic-metadata">

**Author:** [@CohenCyril](https://discourse.rocq-prover.org/u/CohenCyril)\
**Replies:** 0\
**Last updated:** [April 14, 2025, 3:45pm UTC](https://discourse.rocq-prover.org/t/mathcomp-2-4-0-released/2632 "2025-04-14T15:45:36Z")

</div>

We are proud to announce the immediate availability of the Mathematical Components library version 2.4.0. The webpage, and documentation, are available at https://math-comp.github.io/. This release is compatible with C…

---

## [Ninth Mathcomp sharing day](https://discourse.rocq-prover.org/t/ninth-mathcomp-sharing-day/2579)

<div class="topic-metadata">

**Author:** [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Replies:** 0\
**Last updated:** [March 24, 2025, 3:57pm UTC](https://discourse.rocq-prover.org/t/ninth-mathcomp-sharing-day/2579 "2025-03-24T15:57:37Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our ninth “Mathcomp sharing day”. On March 26th 2025, from 10am to 5pm Paris time, mathcomp users, from enthusiasts to experts, are welc…

---

## [Sixth Mathcomp sharing day](https://discourse.rocq-prover.org/t/sixth-mathcomp-sharing-day/2430)

<div class="topic-metadata">

**Author:** [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Replies:** 0\
**Last updated:** [September 18, 2024, 11:48am UTC](https://discourse.rocq-prover.org/t/sixth-mathcomp-sharing-day/2430 "2024-09-18T11:48:15Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our sixth “Mathcomp sharing day”. On September 25th 2024, from 9am to 5pm Paris time, mathcomp users, from enthusiasts to experts, are w…

---

## [Second Mathcomp sharing day](https://discourse.rocq-prover.org/t/second-mathcomp-sharing-day/2300)

<div class="topic-metadata">

**Author:** [@CohenCyril](https://discourse.rocq-prover.org/u/CohenCyril)\
**Replies:** 0\
**Last updated:** [May 22, 2024, 9:49am UTC](https://discourse.rocq-prover.org/t/second-mathcomp-sharing-day/2300 "2024-05-22T09:49:58Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our first “Mathcomp sharing day”. On May 29th 2024, From 9am to 5pm Paris time, mathcomp users, from enthusiasts to experts, are welcome…

---

## [First Mathcomp sharing day](https://discourse.rocq-prover.org/t/first-mathcomp-sharing-day/2256)

<div class="topic-metadata">

**Author:** [@CohenCyril](https://discourse.rocq-prover.org/u/CohenCyril)\
**Replies:** 1\
**Last updated:** [April 27, 2024, 10:55am UTC](https://discourse.rocq-prover.org/t/first-mathcomp-sharing-day/2256 "2024-04-27T10:55:14Z")

</div>

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our first “Mathcomp sharing day”. On April 24th 2024, From 10am to 5pm Paris time, mathcomp users, from enthusiasts to experts, are welc…

---

## [Algebra Tactics 1.1.1 released](https://discourse.rocq-prover.org/t/algebra-tactics-1-1-1-released/1929)

<div class="topic-metadata">

**Author:** [@pi8027](https://discourse.rocq-prover.org/u/pi8027)\
**Replies:** 0\
**Last updated:** [April 13, 2023, 1:12pm UTC](https://discourse.rocq-prover.org/t/algebra-tactics-1-1-1-released/1929 "2023-04-13T13:12:33Z")

</div>

Dear Mathematical Components users, We are pleased to announce the release of Algebra Tactics 1.1.1. In addition to the already provided ring and field tactics, this release gives access to the lra, nra and psatz tact…

---

## [Deriving: a library for deriving class instances for inductive types](https://discourse.rocq-prover.org/t/deriving-a-library-for-deriving-class-instances-for-inductive-types/1228)

<div class="topic-metadata">

**Author:** [@arthuraa](https://discourse.rocq-prover.org/u/arthuraa)\
**Replies:** 3\
**Last updated:** [October 4, 2021, 11:59am UTC](https://discourse.rocq-prover.org/t/deriving-a-library-for-deriving-class-instances-for-inductive-types/1228 "2021-10-04T11:59:33Z")

</div>

Hi everyone, I would like to announce the release of Deriving v0.1.0 (https://github.com/arthuraa/deriving, available as coq-deriving on OPAM). It is a library for automating the generation of MathComp class instances f…

---

## [A formal proof of Abel-Ruffini Theorem in Coq](https://discourse.rocq-prover.org/t/a-formal-proof-of-abel-ruffini-theorem-in-coq/1189)

<div class="topic-metadata">

**Author:** [@CohenCyril](https://discourse.rocq-prover.org/u/CohenCyril)\
**Replies:** 0\
**Last updated:** [January 13, 2021, 5:07pm UTC](https://discourse.rocq-prover.org/t/a-formal-proof-of-abel-ruffini-theorem-in-coq/1189 "2021-01-13T17:07:51Z")

</div>

Dear Coq community, I am happy to announce that we – Sophie Bernard, Cyril Cohen, Assia Mahboubi and Pierre-Yves Strub – were able to formalize in Coq a proof of Abel-Ruffini Theorem, which states that there are polynom…