This morning I was thinking about the layout of the search results. Cathy suggested the layout should be like what you get on google where you have a first line which is a link to the result (in our case something like “Lemma 7.69.1”) and then, in smaller font, some content which (hopefully) helps you see at a glance what “Lemma 7.69.1” is all about.
Now if you look at the LaTeX code for “Lemma 7.69.1” then you get:
\begin{lemma}
\label{lemma-resolution-by-finite-free}
Let $R$ be a ring. Let $M$ be an $R$-module.
\begin{enumerate}
\item The exists an exact complex
$$
\ldots \to F_2 \to F_1 \to F_0 \to M \to 0.
$$
with $F_i$ free $R$-modules.
\item If $R$ is Noetherian and $M$ finite $R$, then we
choose the complex such that each $F_i$ is finite free.
In other words, we may find an exact complex
$$
\ldots \to R^{n_2} \to R^{n_1} \to R^{n_0} \to M \to 0.
$$
\end{enumerate}
\end{lemma}
But what is the lemma really saying? Well, if I wanted to tell a student or a colleague what it says I would say something like “Modules have free resolutions.” or “Finite modules over a Noetherian ring have a resolution by finite free modules.” (By the way, this already points to a potential problem with this lemma. We should really have had two lemmas, one dealing with the general case and one dealing with the finite over Noetherian case.)
Anyway, it is technologically easy to add this kind of human readable descriptions to the Stacks project. Namely, we could change the start of the LaTeX code above to
\begin{lemma}
\label{lemma-resolution-by-finite-free}
% Modules have free resolutions and finite modules over a
% Noetherian ring have a resolution by finite free modules.
Let $R$ be a ring. Let $M$ be an $R$-module.
\begin{lemma}
\label{lemma-resolution-by-finite-free}
% Human:
% Modules have free resolutions and finite modules over a
% Noetherian ring have a resolution by finite free modules.
% Ref:
% MatCA, page 73
% Hist:
% Goes back at least to Hilbert.
Let $R$ be a ring. Let $M$ be an $R$-module.
Of course, the problem (as usual) is to find somebody who is willing to add human readable descriptions to each and every lemma, proposition, theorem, remark, situation, etc. Since there are 5889 lemmas, 161 propositions, 134 theorems, 471 remarks, 46 situations this is no mean task! (It will take about 100 hours to do this if you can do one of these per minute. Come on guys, that is only 10 days of hard work! And with a group of 10 people…)
We should have done this from the start! Hmm…
