## The problem.

I really want to do computer-assisted proofs. Actually I am looking forward to decades of computer assisted proof writing. But so far it has not been going well. One reason is that libraries are either not there or not accessible.

## Examples.

This is the official reference for Mathematical Components, the Coq Mathematics standard. Yes, it is an alphabetical index of identifiers. Sounds great, right? *(Not really. A reference should have a structure — a tree of contents.)* Suppose I am looking for the Gauss’s lemma concerning polynomials. Well, that would be on page *g*, right? So I am in luck!

Gauss_gcdl [lemma, in mathcomp.ssreflect.div]

Gauss_gcdr [lemma, in mathcomp.ssreflect.div]

Gauss_dvdl [lemma, in mathcomp.ssreflect.div]

Gauss_dvdr [lemma, in mathcomp.ssreflect.div]

Gauss_dvd [lemma, in mathcomp.ssreflect.div]

Gauss_gcdzl [lemma, in mathcomp.algebra.intdiv]

Gauss_gcdzr [lemma, in mathcomp.algebra.intdiv]

Gauss_dvdzl [lemma, in mathcomp.algebra.intdiv]

Gauss_dvdzr [lemma, in mathcomp.algebra.intdiv]

Gauss_dvdz [lemma, in mathcomp.algebra.intdiv]

Oh… Well, Gauss has a lot of mathematics to his name. Maybe the one I need is one of these. But which?

How about the Rational Root Theorem? Unfortunately the word *«rational»* does not appear anywhere on page *r*.

Maybe I should look elsewhere? This module looks like it might be related. Unfortunately the definitions herein do not appear in the index. The theorems are named like `nvar0_mpolyC_eq`

, so it is hard to tell if the result I am looking for is there or not.

So:

- There is no structured reference.
- There are no comments to most definitions.
- Naming is a disaster.

I do not mean to bash specifically this library. I mean, look at the standard library that goes with the installation of Coq.

BinNatDef BinNat Nnat Ndigits Ndist Ndec Ndiv_def Ngcd_def Nsqrt_def (NArith)

Oh… Well, at least sometimes it has readable names and comments.

## My explanation.

What is going on? Is the style of these works officially considered a good style for writing Coq? Or am I unlucky to stumble upon particularly thorny examples and to miss all the beautiful flowers?

I think this disaster is systematic and the reason for it is habit and the system of motivation that supports it.

- Software engineers are expected to maintain their work, so it must be made clear and accessible. I am a software engineer — I need proofs to help me and my team continuously deliver correct software.
- Research mathematicians are only expected to publish a result once and for a relatively local audience, so who cares if the devil himself would break a leg wading through their code. The code is an appendix №
*n*of an appendix №*m*. People that write the libraries mentioned above are research mathematicians.

## What next?

But, as I mentioned, I am looking forward to decades of computer assisted proof writing. And it looks like Coq will be the prime proof assistant in the foreseeable future. So I may as well re-write the works mentioned above if I feel like it.

- Should I?
- What should my plan be for getting a standard library that would make my efforts in proof writing more effective?
- How do I make sure it helps others too? How do I blaze a trail?
- Am I going to make more friends than enemies along the way?